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