Theorem axnulALT2

Description: Alternate proof of axnul , proved from propositional calculus, ax-gen , ax-4 , ax-5 , and ax-inf2 . (Contributed by BTernaryTau, 22-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axnulALT2	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		exsimpr	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
2		ax-inf2	⊢ ∃ 𝑧 ( ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ( 𝑦 ∈ 𝑧 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑦 ↔ ( 𝑤 ∈ 𝑥 ∨ 𝑤 = 𝑥 ) ) ) ) )
3		simpl	⊢ ( ( ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ( 𝑦 ∈ 𝑧 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑦 ↔ ( 𝑤 ∈ 𝑥 ∨ 𝑤 = 𝑥 ) ) ) ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
4	2 3	eximii	⊢ ∃ 𝑧 ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
5	1 4	exlimiiv	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥