Metamath Proof Explorer

Theorem axnulALT

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , sp , and ax-rep . To check this, replace sp with the obsolete axiom ax-c5 in the proof of axnulALT and type the Metamath program "MM> SHOW TRACE__BACK axnulALT / AXIOMS" command. (Contributed by Jeff Hoffman, 3-Feb-2008) (Proof shortened by Mario Carneiro, 17-Nov-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axnulALT ⊢ ∃ x ∀ y ¬ y ∈ x

Proof

Step Hyp Ref Expression
1 ax-rep ⊢ ∀ w ∃ x ∀ y ∀ x ⊥ → y = x → ∃ x ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
2 sp ⊢ ∀ x ¬ ∀ y ∀ x ⊥ → y = x → ¬ ∀ y ∀ x ⊥ → y = x
3 2 con2i ⊢ ∀ y ∀ x ⊥ → y = x → ¬ ∀ x ¬ ∀ y ∀ x ⊥ → y = x
4 df-ex ⊢ ∃ x ∀ y ∀ x ⊥ → y = x ↔ ¬ ∀ x ¬ ∀ y ∀ x ⊥ → y = x
5 3 4 sylibr ⊢ ∀ y ∀ x ⊥ → y = x → ∃ x ∀ y ∀ x ⊥ → y = x
6 fal ⊢ ¬ ⊥
7 sp ⊢ ∀ x ⊥ → ⊥
8 6 7 mto ⊢ ¬ ∀ x ⊥
9 8 pm2.21i ⊢ ∀ x ⊥ → y = x
10 5 9 mpg ⊢ ∃ x ∀ y ∀ x ⊥ → y = x
11 1 10 mpg ⊢ ∃ x ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
12 8 intnan ⊢ ¬ w ∈ z ∧ ∀ x ⊥
13 12 nex ⊢ ¬ ∃ w w ∈ z ∧ ∀ x ⊥
14 13 nbn ⊢ ¬ y ∈ x ↔ y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
15 14 albii ⊢ ∀ y ¬ y ∈ x ↔ ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
16 15 exbii ⊢ ∃ x ∀ y ¬ y ∈ x ↔ ∃ x ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
17 11 16 mpbir ⊢ ∃ x ∀ y ¬ y ∈ x