Theorem dtruALT2

Description: Alternate proof of dtru using ax-pr instead of ax-pow . (Contributed by Mario Carneiro, 31-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dtruALT2	|- -. A. x x = y

Proof

Step	Hyp	Ref	Expression
1		0inp0	|- ( y = (/) -> -. y = { (/) } )
2		snex	|- { (/) } e. _V
3		eqeq2	|- ( x = { (/) } -> ( y = x <-> y = { (/) } ) )
4	3	notbid	|- ( x = { (/) } -> ( -. y = x <-> -. y = { (/) } ) )
5	2 4	spcev	|- ( -. y = { (/) } -> E. x -. y = x )
6	1 5	syl	|- ( y = (/) -> E. x -. y = x )
7		0ex	|- (/) e. _V
8		eqeq2	|- ( x = (/) -> ( y = x <-> y = (/) ) )
9	8	notbid	|- ( x = (/) -> ( -. y = x <-> -. y = (/) ) )
10	7 9	spcev	|- ( -. y = (/) -> E. x -. y = x )
11	6 10	pm2.61i	|- E. x -. y = x
12		exnal	|- ( E. x -. y = x <-> -. A. x y = x )
13		eqcom	|- ( y = x <-> x = y )
14	13	albii	|- ( A. x y = x <-> A. x x = y )
15	12 14	xchbinx	|- ( E. x -. y = x <-> -. A. x x = y )
16	11 15	mpbi	|- -. A. x x = y