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

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ power x ≠ x
Tactic:
intro h
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x = x
⊢ False

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x = x
⊢ False
Tactic:
exact (power_not_subset x) (subset_of_eq h)
State after:
no goals