Theorem sn-dtru

Description: dtru without ax-8 or ax-12 . (Contributed by SN, 21-Sep-2023)

	Ref	Expression
Assertion	sn-dtru	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		sn-el	⊢ ∃ 𝑤 ∃ 𝑥 𝑥 ∈ 𝑤
2		ax-nul	⊢ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧
3		exdistrv	⊢ ( ∃ 𝑤 ∃ 𝑧 ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑤 ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) )
4	1 2 3	mpbir2an	⊢ ∃ 𝑤 ∃ 𝑧 ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 )
5		ax9v1	⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧 ) )
6	5	eximdv	⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑥 𝑥 ∈ 𝑤 → ∃ 𝑥 𝑥 ∈ 𝑧 ) )
7		df-ex	⊢ ( ∃ 𝑥 𝑥 ∈ 𝑧 ↔ ¬ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 )
8	6 7	syl6ib	⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑥 𝑥 ∈ 𝑤 → ¬ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) )
9		imnan	⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝑤 → ¬ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ↔ ¬ ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) )
10	8 9	sylib	⊢ ( 𝑤 = 𝑧 → ¬ ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) )
11	10	con2i	⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) → ¬ 𝑤 = 𝑧 )
12	11	2eximi	⊢ ( ∃ 𝑤 ∃ 𝑧 ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) → ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 )
13		equeuclr	⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 𝑦 → 𝑤 = 𝑧 ) )
14	13	con3d	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ¬ 𝑤 = 𝑦 ) )
15		ax7v1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → 𝑤 = 𝑦 ) )
16	15	con3d	⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
17	16	spimevw	⊢ ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
18	14 17	syl6	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
19		ax7v1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) )
20	19	con3d	⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) )
21	20	spimevw	⊢ ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
22	21	a1d	⊢ ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) )
23	18 22	pm2.61i	⊢ ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
24	23	exlimivv	⊢ ( ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 )
25	4 12 24	mp2b	⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦
26		exnal	⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
27	25 26	mpbi	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦