Proof 01. 1 ⊢ ¬A = ∅, hypo. 02. 2 ⊢ ¬∃x. x ∈ A, hypo. 03. 2 ⊢ ∀x. ¬x ∈ A, neg_ex 2. 04. 2 ⊢ A = ∅, set_with_no_elements 3. 05. 1, 2 ⊢ ⊥, neg_elim 1 4. 06. 1 ⊢ ¬¬∃x. x ∈ A, neg_intro 5. 07. 1 ⊢ ∃x. x ∈ A, dne 6. non_empty. ⊢ ¬A = ∅ → ∃x. x ∈ A, subj_intro 7.
Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, lem.