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

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : x = y
⊢ x ⊆ y
Tactic:
subst h
State after:
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ x ⊆ x

State before:
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ x ⊆ x
Tactic:
exact subset_rfl
State after:
no goals