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∀yy∈x↔∃ww∈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∀yy∈x↔∃ww∈z∧∀x⊥
12 8 intnan ⊢¬w∈z∧∀x⊥
13 12 nex ⊢¬∃ww∈z∧∀x⊥
14 13 nbn ⊢¬y∈x↔y∈x↔∃ww∈z∧∀x⊥
15 14 albii ⊢∀y¬y∈x↔∀yy∈x↔∃ww∈z∧∀x⊥
16 15 exbii ⊢∃x∀y¬y∈x↔∃x∀yy∈x↔∃ww∈z∧∀x⊥
17 11 16 mpbir ⊢∃x∀y¬y∈x