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

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

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ ∅ ∪ x ↔ z✝ ∈ x
Tactic:
simp
State after:
no goals