Theorem bj-dtru

Description: Remove dependency on ax-13 from dtru . (Contributed by BJ, 31-May-2019)

TODO: This predates the removal of ax-13 in dtru . But actually, sn-dtru is better than either, so move it to Main with sn-el (and determine whether bj-dtru should be kept as ALT or deleted).

(Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-dtru	|- -. A. x x = y

Proof

Step	Hyp	Ref	Expression
1		el	|- E. w x e. w
2		ax-nul	|- E. z A. x -. x e. z
3		sp	|- ( A. x -. x e. z -> -. x e. z )
4	2 3	eximii	|- E. z -. x e. z
5		exdistrv	|- ( E. w E. z ( x e. w /\ -. x e. z ) <-> ( E. w x e. w /\ E. z -. x e. z ) )
6	1 4 5	mpbir2an	|- E. w E. z ( x e. w /\ -. x e. z )
7		ax9	|- ( w = z -> ( x e. w -> x e. z ) )
8	7	com12	|- ( x e. w -> ( w = z -> x e. z ) )
9	8	con3dimp	|- ( ( x e. w /\ -. x e. z ) -> -. w = z )
10	9	2eximi	|- ( E. w E. z ( x e. w /\ -. x e. z ) -> E. w E. z -. w = z )
11	6 10	ax-mp	|- E. w E. z -. w = z
12		equequ2	|- ( z = y -> ( w = z <-> w = y ) )
13	12	notbid	|- ( z = y -> ( -. w = z <-> -. w = y ) )
14		ax7	|- ( x = w -> ( x = y -> w = y ) )
15	14	con3d	|- ( x = w -> ( -. w = y -> -. x = y ) )
16	15	spimevw	|- ( -. w = y -> E. x -. x = y )
17	13 16	syl6bi	|- ( z = y -> ( -. w = z -> E. x -. x = y ) )
18		ax7	|- ( x = z -> ( x = y -> z = y ) )
19	18	con3d	|- ( x = z -> ( -. z = y -> -. x = y ) )
20	19	spimevw	|- ( -. z = y -> E. x -. x = y )
21	20	a1d	|- ( -. z = y -> ( -. w = z -> E. x -. x = y ) )
22	17 21	pm2.61i	|- ( -. w = z -> E. x -. x = y )
23	22	exlimivv	|- ( E. w E. z -. w = z -> E. x -. x = y )
24	11 23	ax-mp	|- E. x -. x = y
25		exnal	|- ( E. x -. x = y <-> -. A. x x = y )
26	24 25	mpbi	|- -. A. x x = y