This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dtruALT2

Description: Alternate proof of dtru using ax-pow instead of ax-pr . See dtruALT for another proof using ax-pow instead of ax-pr . (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by BJ, 31-May-2019) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dtruALT2 ⊢ ¬ ∀ x x = y

Proof

Step Hyp Ref Expression
1 elALT2 ⊢ ∃ w x ∈ w
2 ax-nul ⊢ ∃ z ∀ x ¬ x ∈ z
3 elequ1 ⊢ x = w → x ∈ z ↔ w ∈ z
4 3 notbid ⊢ x = w → ¬ x ∈ z ↔ ¬ w ∈ z
5 4 spw ⊢ ∀ x ¬ x ∈ z → ¬ x ∈ z
6 2 5 eximii ⊢ ∃ z ¬ x ∈ z
7 exdistrv ⊢ ∃ w ∃ z x ∈ w ∧ ¬ x ∈ z ↔ ∃ w x ∈ w ∧ ∃ z ¬ x ∈ z
8 1 6 7 mpbir2an ⊢ ∃ w ∃ z x ∈ w ∧ ¬ x ∈ z
9 ax9v2 ⊢ w = z → x ∈ w → x ∈ z
10 9 com12 ⊢ x ∈ w → w = z → x ∈ z
11 10 con3dimp ⊢ x ∈ w ∧ ¬ x ∈ z → ¬ w = z
12 11 2eximi ⊢ ∃ w ∃ z x ∈ w ∧ ¬ x ∈ z → ∃ w ∃ z ¬ w = z
13 equequ2 ⊢ z = y → w = z ↔ w = y
14 13 notbid ⊢ 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 biimtrdi ⊢ 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 8 12 24 mp2b ⊢ ∃ x ¬ x = y
26 exnal ⊢ ∃ x ¬ x = y ↔ ¬ ∀ x x = y
27 25 26 mpbi ⊢ ¬ ∀ x x = y