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

Proof

Step Hyp Ref Expression
1 sn-el 
 |-  E. w E. x x e. w
2 ax-nul 
 |-  E. z A. x -. x e. z
3 exdistrv 
 |-  ( E. w E. z ( E. x x e. w /\ A. x -. x e. z ) <-> ( E. w E. x x e. w /\ E. z A. x -. x e. z ) )
4 1 2 3 mpbir2an 
 |-  E. w E. z ( E. x x e. w /\ A. x -. x e. z )
5 ax9v1 
 |-  ( w = z -> ( x e. w -> x e. z ) )
6 5 eximdv 
 |-  ( w = z -> ( E. x x e. w -> E. x x e. z ) )
7 df-ex 
 |-  ( E. x x e. z <-> -. A. x -. x e. z )
8 6 7 syl6ib 
 |-  ( w = z -> ( E. x x e. w -> -. A. x -. x e. z ) )
9 imnan 
 |-  ( ( E. x x e. w -> -. A. x -. x e. z ) <-> -. ( E. x x e. w /\ A. x -. x e. z ) )
10 8 9 sylib 
 |-  ( w = z -> -. ( E. x x e. w /\ A. x -. x e. z ) )
11 10 con2i 
 |-  ( ( E. x x e. w /\ A. x -. x e. z ) -> -. w = z )
12 11 2eximi 
 |-  ( E. w E. z ( E. x x e. w /\ A. x -. x e. z ) -> E. w E. 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 -> E. x -. x = y )
18 14 17 syl6 
 |-  ( 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 4 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