Theorem: SetTheory.subset_antisymm (SetTheory/Basic.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
h₁ : x ⊆ y
h₂ : y ⊆ x
⊢ x = y
Tactic:
ext
State after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z : V
h₁ : x ⊆ y
h₂ : y ⊆ x
z✝ : V
⊢ z✝ ∈ x ↔ z✝ ∈ y

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z : V
h₁ : x ⊆ y
h₂ : y ⊆ x
z✝ : V
⊢ z✝ ∈ x ↔ z✝ ∈ y
Tactic:
aesop
State after:
no goals