Theorem ax6e2ndVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd is ax6e2ndVD without virtual deductions and was automatically derived from ax6e2ndVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2ndVD	|- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- u e. _V
2		ax6e	|- E. y y = v
3	1 2	pm3.2i	|- ( u e. _V /\ E. y y = v )
4		19.42v	|- ( E. y ( u e. _V /\ y = v ) <-> ( u e. _V /\ E. y y = v ) )
5	4	biimpri	|- ( ( u e. _V /\ E. y y = v ) -> E. y ( u e. _V /\ y = v ) )
6	3 5	e0a	|- E. y ( u e. _V /\ y = v )
7		isset	|- ( u e. _V <-> E. x x = u )
8	7	anbi1i	|- ( ( u e. _V /\ y = v ) <-> ( E. x x = u /\ y = v ) )
9	8	exbii	|- ( E. y ( u e. _V /\ y = v ) <-> E. y ( E. x x = u /\ y = v ) )
10	6 9	mpbi	|- E. y ( E. x x = u /\ y = v )
11		idn1	|- (. -. A. x x = y ->. -. A. x x = y ).
12		hbnae	|- ( -. A. x x = y -> A. y -. A. x x = y )
13		hbn1	|- ( -. A. x x = y -> A. x -. A. x x = y )
14		ax-5	|- ( z = v -> A. x z = v )
15		ax-5	|- ( y = v -> A. z y = v )
16		idn1	|- (. z = y ->. z = y ).
17		equequ1	|- ( z = y -> ( z = v <-> y = v ) )
18	16 17	e1a	|- (. z = y ->. ( z = v <-> y = v ) ).
19	18	in1	|- ( z = y -> ( z = v <-> y = v ) )
20	14 15 19	dvelimh	|- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
21	11 20	e1a	|- (. -. A. x x = y ->. ( y = v -> A. x y = v ) ).
22	21	in1	|- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
23	22	alimi	|- ( A. x -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
24	13 23	syl	|- ( -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
25	11 24	e1a	|- (. -. A. x x = y ->. A. x ( y = v -> A. x y = v ) ).
26		19.41rg	|- ( A. x ( y = v -> A. x y = v ) -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
27	25 26	e1a	|- (. -. A. x x = y ->. ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) ).
28	27	in1	|- ( -. A. x x = y -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
29	28	alimi	|- ( A. y -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
30	12 29	syl	|- ( -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
31	11 30	e1a	|- (. -. A. x x = y ->. A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) ).
32		exim	|- ( A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) -> ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) )
33	31 32	e1a	|- (. -. A. x x = y ->. ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) ).
34		pm2.27	|- ( E. y ( E. x x = u /\ y = v ) -> ( ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) -> E. y E. x ( x = u /\ y = v ) ) )
35	10 33 34	e01	|- (. -. A. x x = y ->. E. y E. x ( x = u /\ y = v ) ).
36		excomim	|- ( E. y E. x ( x = u /\ y = v ) -> E. x E. y ( x = u /\ y = v ) )
37	35 36	e1a	|- (. -. A. x x = y ->. E. x E. y ( x = u /\ y = v ) ).
38	37	in1	|- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )