Metamath Proof Explorer

Theorem sn-dtru

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

Ref Expression
Assertion sn-dtru ⊢ ¬ ∀ x x = y

Proof

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