Proof
01. ⊢ ∃A. set A ∧ (∅ ∈ A ∧ ∀x. x ∈ A → x ∪ {x} ∈ A), infinity.
02. 2 ⊢ set A ∧ (∅ ∈ A ∧ ∀x. x ∈ A → x ∪ {x} ∈ A), hypo.
03. 2 ⊢ ∅ ∈ A, conj_elimrl 2.
04. 2 ⊢ set ∅, set_intro 3.
empty_set_is_set. ⊢ set ∅, ex_elim 1 4.
Dependencies
The given proof depends on one axiom:
infinity.