Theorem ax6e2eq

Description: Alternate form of ax6e for non-distinct x , y and u = v . ax6e2eq is derived from ax6e2eqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2eq	$$⊢\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		ax6ev	$$⊢\exists xx=u$$
2		hbae	$$⊢\forall xx=y\to \forall x\forall xx=y$$
3		ax7	$$⊢x=y\to \left(x=u\to y=u\right)$$
4	3	sps	$$⊢\forall xx=y\to \left(x=u\to y=u\right)$$
5	4	ancld	$$⊢\forall xx=y\to \left(x=u\to \left(x=u\wedge y=u\right)\right)$$
6	2 5	eximdh	$$⊢\forall xx=y\to \left(\exists xx=u\to \exists x\left(x=u\wedge y=u\right)\right)$$
7	1 6	mpi	$$⊢\forall xx=y\to \exists x\left(x=u\wedge y=u\right)$$
8	7	axc4i	$$⊢\forall xx=y\to \forall x\exists x\left(x=u\wedge y=u\right)$$
9		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)$$
10	8 9	mpd	$$⊢\forall xx=y\to \forall y\exists x\left(x=u\wedge y=u\right)$$
11		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)$$
12	10 11	syl	$$⊢\forall xx=y\to \exists y\exists x\left(x=u\wedge y=u\right)$$
13		excomim	$$⊢\exists y\exists x\left(x=u\wedge y=u\right)\to \exists x\exists y\left(x=u\wedge y=u\right)$$
14	12 13	syl	$$⊢\forall xx=y\to \exists x\exists y\left(x=u\wedge y=u\right)$$
15		equtrr	$$⊢u=v\to \left(y=u\to y=v\right)$$
16	15	anim2d	$$⊢u=v\to \left(\left(x=u\wedge y=u\right)\to \left(x=u\wedge y=v\right)\right)$$
17	16	2eximdv	$$⊢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)$$
18	14 17	syl5com	$$⊢\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$