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	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		ax-rep	⊢ ( ∀ 𝑤 ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
2		fal	⊢ ¬ ⊥
3	2	spfalw	⊢ ( ∀ 𝑥 ⊥ → ⊥ )
4	2 3	mto	⊢ ¬ ∀ 𝑥 ⊥
5	4	pm2.21i	⊢ ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 )
6	5	ax-gen	⊢ ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 )
7	6	exgen	⊢ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ⊥ → 𝑦 = 𝑥 )
8	1 7	mpg	⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) )
9	4	intnan	⊢ ¬ ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ )
10	9	nex	⊢ ¬ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ )
11	10	nbn	⊢ ( ¬ 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
12	11	albii	⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
13	12	exbii	⊢ ( ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑥 ⊥ ) ) )
14	8 13	mpbir	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥