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 
|- -. A. x x = y

Proof

Step Hyp Ref Expression
1 elALT2 
 |-  E. w x e. w
2 ax-nul 
 |-  E. z A. x -. x e. z
3 elequ1 
 |-  ( x = w -> ( x e. z <-> w e. z ) )
4 3 notbid 
 |-  ( x = w -> ( -. x e. z <-> -. w e. z ) )
5 4 spw 
 |-  ( A. x -. x e. z -> -. x e. z )
6 2 5 eximii 
 |-  E. z -. x e. z
7 exdistrv 
 |-  ( E. w E. z ( x e. w /\ -. x e. z ) <-> ( E. w x e. w /\ E. z -. x e. z ) )
8 1 6 7 mpbir2an 
 |-  E. w E. z ( x e. w /\ -. x e. z )
9 ax9v2 
 |-  ( w = z -> ( x e. w -> x e. z ) )
10 9 com12 
 |-  ( x e. w -> ( w = z -> x e. z ) )
11 10 con3dimp 
 |-  ( ( x e. w /\ -. x e. z ) -> -. w = z )
12 11 2eximi 
 |-  ( E. w E. z ( x e. w /\ -. x e. z ) -> E. w E. 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 -> E. x -. x = y )
18 14 17 biimtrdi 
 |-  ( z = y -> ( -. w = z -> E. 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 -> E. x -. x = y )
22 21 a1d 
 |-  ( -. z = y -> ( -. w = z -> E. x -. x = y ) )
23 18 22 pm2.61i 
 |-  ( -. w = z -> E. x -. x = y )
24 23 exlimivv 
 |-  ( E. w E. z -. w = z -> E. x -. x = y )
25 8 12 24 mp2b 
 |-  E. x -. x = y
26 exnal 
 |-  ( E. x -. x = y <-> -. A. x x = y )
27 25 26 mpbi 
 |-  -. A. x x = y