Theorem: SetTheory.ext_iff (SetTheory/Axioms.lean)

State before:
V : Type u_1
inst✝² inst✝¹ : SetTheory V
inst✝ : Extensionality V
x y : V
⊢ x = y → ∀ (z : V), z ∈ x ↔ z ∈ y
Tactic:
aesop
State after:
no goals