Theorem axnulregtco

Description: Derivation of ax-nul from ax-reg and ax-tco . Use ax-nul instead. (Contributed by Matthew House, 7-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤 ) )
2	1	biimprd	⊢ ( 𝑥 = 𝑧 → ( 𝑧 ∈ 𝑤 → 𝑥 ∈ 𝑤 ) )
3	2	spimevw	⊢ ( 𝑧 ∈ 𝑤 → ∃ 𝑥 𝑥 ∈ 𝑤 )
4		ax-reg	⊢ ( ∃ 𝑥 𝑥 ∈ 𝑤 → ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) ) )
5	3 4	syl	⊢ ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) ) )
6		pm2.65	⊢ ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) → ( ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) → ¬ 𝑦 ∈ 𝑥 ) )
7	6	al2imi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) → ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
8	7	imim2i	⊢ ( ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) ) → ( 𝑥 ∈ 𝑤 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) → ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) ) )
9	8	impd	⊢ ( ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) ) → ( ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) ) → ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
10	9	aleximi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑤 ) ) → ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
11	5 10	mpan9	⊢ ( ( 𝑧 ∈ 𝑤 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) ) ) → ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
12		ax-tco	⊢ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑤 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑤 ) ) )
13	11 12	exlimiiv	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥