Metamath Proof Explorer

Theorem axnulALT2

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , ax-6 , and ax-rep . (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BTernaryTau, 27-Mar-2026)

Ref Expression
Assertion axnulALT2 ⊢ ∃ 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 fal ⊢ ¬ ⊥
3 2 spfalw ⊢ ∀ x ⊥ → ⊥
4 2 3 mto ⊢ ¬ ∀ x ⊥
5 4 pm2.21i ⊢ ∀ x ⊥ → y = x
6 5 ax-gen ⊢ ∀ y ∀ x ⊥ → y = x
7 6 exgen ⊢ ∃ x ∀ y ∀ x ⊥ → y = x
8 1 7 mpg ⊢ ∃ x ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
9 4 intnan ⊢ ¬ w ∈ z ∧ ∀ x ⊥
10 9 nex ⊢ ¬ ∃ w w ∈ z ∧ ∀ x ⊥
11 10 nbn ⊢ ¬ y ∈ x ↔ y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
12 11 albii ⊢ ∀ y ¬ y ∈ x ↔ ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
13 12 exbii ⊢ ∃ x ∀ y ¬ y ∈ x ↔ ∃ x ∀ y y ∈ x ↔ ∃ w w ∈ z ∧ ∀ x ⊥
14 8 13 mpbir ⊢ ∃ x ∀ y ¬ y ∈ x