Theorem: SetTheory.empty_mem_ω (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
⊢ ∅ ∈ ω
Tactic:
rw [mem_ω_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
⊢ ∀ (s : V), Inductive s → ∅ ∈ s

State before:
V : Type u_1
inst✝ : Zermelo V
⊢ ∀ (s : V), Inductive s → ∅ ∈ s
Tactic:
intro s hs
State after:
V : Type u_1
inst✝ : Zermelo V
s : V
hs : Inductive s
⊢ ∅ ∈ s

State before:
V : Type u_1
inst✝ : Zermelo V
s : V
hs : Inductive s
⊢ ∅ ∈ s
Tactic:
exact hs.empty_mem
State after:
no goals