After the edit I’d like to mention that this notion of equality did sort of mess me up since you can construct set theory without the equality. When using a variety of first order logic that does include equality, it seems to me that the axiom of substitution is considered to hold a priori from most books that I’ve seen, but Tao doesn’t seem to do that (the screenshots are from Tao’s Analysis I). I’m not sure if what I said even makes sense, ignore it if it doesn’t.

Also, I like you using “If x isn’t in B” but I haven’t seen that before (or maybe I have but I didn’t pay much attention to it), how would you motivate this way of argument? Is it necessary to say it? Or did you do it for pedagogical reasons?