Theorem ax6e2eqVD

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. ax6e2eq is ax6e2eqVD without virtual deductions and was automatically derived from ax6e2eqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2eqVD	$$⊢\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(\forall xx=y\to \forall xx=y\right)$$
2		ax6ev	$$⊢\exists xx=u$$
3		hba1	$$⊢\forall xx=y\to \forall x\forall xx=y$$
4		sp	$$⊢\forall x\forall xx=y\to \forall xx=y$$
5	3 4	impbii	$$⊢\forall xx=y\leftrightarrow \forall x\forall xx=y$$
6		idn2	$$⊢\left(\forall xx=y,x=u\to x=u\right)$$
7		sp	$$⊢\forall xx=y\to x=y$$
8	1 7	e1a	$$⊢\left(\forall xx=y\to x=y\right)$$
9		ax7	$$⊢x=y\to \left(x=u\to y=u\right)$$
10	9	com12	$$⊢x=u\to \left(x=y\to y=u\right)$$
11	6 8 10	e21	$$⊢\left(\forall xx=y,x=u\to y=u\right)$$
12		pm3.2	$$⊢x=u\to \left(y=u\to \left(x=u\wedge y=u\right)\right)$$
13	6 11 12	e22	$$⊢\left(\forall xx=y,x=u\to \left(x=u\wedge y=u\right)\right)$$
14	13	in2	$$⊢\left(\forall xx=y\to \left(x=u\to \left(x=u\wedge y=u\right)\right)\right)$$
15	14	in1	$$⊢\forall xx=y\to \left(x=u\to \left(x=u\wedge y=u\right)\right)$$
16	15	alimi	$$⊢\forall x\forall xx=y\to \forall x\left(x=u\to \left(x=u\wedge y=u\right)\right)$$
17	5 16	sylbi	$$⊢\forall xx=y\to \forall x\left(x=u\to \left(x=u\wedge y=u\right)\right)$$
18	1 17	e1a	$$⊢\left(\forall xx=y\to \forall x\left(x=u\to \left(x=u\wedge y=u\right)\right)\right)$$
19		exim	$$⊢\forall x\left(x=u\to \left(x=u\wedge y=u\right)\right)\to \left(\exists xx=u\to \exists x\left(x=u\wedge y=u\right)\right)$$
20	18 19	e1a	$$⊢\left(\forall xx=y\to \left(\exists xx=u\to \exists x\left(x=u\wedge y=u\right)\right)\right)$$
21		pm2.27	$$⊢\exists xx=u\to \left(\left(\exists xx=u\to \exists x\left(x=u\wedge y=u\right)\right)\to \exists x\left(x=u\wedge y=u\right)\right)$$
22	2 20 21	e01	$$⊢\left(\forall xx=y\to \exists x\left(x=u\wedge y=u\right)\right)$$
23	22	in1	$$⊢\forall xx=y\to \exists x\left(x=u\wedge y=u\right)$$
24	23	axc4i	$$⊢\forall xx=y\to \forall x\exists x\left(x=u\wedge y=u\right)$$
25	1 24	e1a	$$⊢\left(\forall xx=y\to \forall x\exists x\left(x=u\wedge y=u\right)\right)$$
26		axc11	$$⊢\forall xx=y\to \left(\forall x\exists x\left(x=u\wedge y=u\right)\to \forall y\exists x\left(x=u\wedge y=u\right)\right)$$
27	1 25 26	e11	$$⊢\left(\forall xx=y\to \forall y\exists x\left(x=u\wedge y=u\right)\right)$$
28		19.2	$$⊢\forall y\exists x\left(x=u\wedge y=u\right)\to \exists y\exists x\left(x=u\wedge y=u\right)$$
29	27 28	e1a	$$⊢\left(\forall xx=y\to \exists y\exists x\left(x=u\wedge y=u\right)\right)$$
30		excomim	$$⊢\exists y\exists x\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=u\right)$$
31	29 30	e1a	$$⊢\left(\forall xx=y\to \exists x\exists y\left(x=u\wedge y=u\right)\right)$$
32		idn1	$$⊢\left(u=v\to u=v\right)$$
33		idn2	$$⊢\left(u=v,\left(x=u\wedge y=u\right)\to \left(x=u\wedge y=u\right)\right)$$
34		simpr	$$⊢\left(x=u\wedge y=u\right)\to y=u$$
35	33 34	e2	$$⊢\left(u=v,\left(x=u\wedge y=u\right)\to y=u\right)$$
36		equtrr	$$⊢u=v\to \left(y=u\to y=v\right)$$
37	32 35 36	e12	$$⊢\left(u=v,\left(x=u\wedge y=u\right)\to y=v\right)$$
38		simpl	$$⊢\left(x=u\wedge y=u\right)\to x=u$$
39	33 38	e2	$$⊢\left(u=v,\left(x=u\wedge y=u\right)\to x=u\right)$$
40		pm3.21	$$⊢y=v\to \left(x=u\to \left(x=u\wedge y=v\right)\right)$$
41	37 39 40	e22	$$⊢\left(u=v,\left(x=u\wedge y=u\right)\to \left(x=u\wedge y=v\right)\right)$$
42	41	in2	$$⊢\left(u=v\to \left(\left(x=u\wedge y=u\right)\to \left(x=u\wedge y=v\right)\right)\right)$$
43	42	gen11	$$⊢\left(u=v\to \forall y\left(\left(x=u\wedge y=u\right)\to \left(x=u\wedge y=v\right)\right)\right)$$
44		exim	$$⊢\forall y\left(\left(x=u\wedge y=u\right)\to \left(x=u\wedge y=v\right)\right)\to \left(\exists y\left(x=u\wedge y=u\right)\to \exists y\left(x=u\wedge y=v\right)\right)$$
45	43 44	e1a	$$⊢\left(u=v\to \left(\exists y\left(x=u\wedge y=u\right)\to \exists y\left(x=u\wedge y=v\right)\right)\right)$$
46	45	gen11	$$⊢\left(u=v\to \forall x\left(\exists y\left(x=u\wedge y=u\right)\to \exists y\left(x=u\wedge y=v\right)\right)\right)$$
47		exim	$$⊢\forall x\left(\exists y\left(x=u\wedge y=u\right)\to \exists y\left(x=u\wedge y=v\right)\right)\to \left(\exists x\exists y\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
48	46 47	e1a	$$⊢\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)$$
49	48	in1	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
50		pm2.04	$$⊢\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\to \left(\exists x\exists y\left(x=u\wedge y=u\right)\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)$$
51	50	com12	$$⊢\exists x\exists y\left(x=u\wedge y=u\right)\to \left(\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)$$
52	31 49 51	e10	$$⊢\left(\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)$$
53	52	in1	$$⊢\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$