This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 x x = y \to (u = v \to \exists x \exists y (x = u \land y = v))$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$⊢ \exists x x = u$
2		hbae	$⊢ \forall x x = y \to \forall x \forall x x = y$
3		ax7	$⊢ x = y \to (x = u \to y = u)$
4	3	sps	$⊢ \forall x x = y \to (x = u \to y = u)$
5	4	ancld	$⊢ \forall x x = y \to (x = u \to (x = u \land y = u))$
6	2 5	eximdh	$⊢ \forall x x = y \to (\exists x x = u \to \exists x (x = u \land y = u))$
7	1 6	mpi	$⊢ \forall x x = y \to \exists x (x = u \land y = u)$
8	7	axc4i	$⊢ \forall x x = y \to \forall x \exists x (x = u \land y = u)$
9		axc11	$⊢ \forall x x = y \to (\forall x \exists x (x = u \land y = u) \to \forall y \exists x (x = u \land y = u))$
10	8 9	mpd	$⊢ \forall x x = y \to \forall y \exists x (x = u \land y = u)$
11		19.2	$⊢ \forall y \exists x (x = u \land y = u) \to \exists y \exists x (x = u \land y = u)$
12	10 11	syl	$⊢ \forall x x = y \to \exists y \exists x (x = u \land y = u)$
13		excomim	$⊢ \exists y \exists x (x = u \land y = u) \to \exists x \exists y (x = u \land y = u)$
14	12 13	syl	$⊢ \forall x x = y \to \exists x \exists y (x = u \land y = u)$
15		equtrr	$⊢ u = v \to (y = u \to y = v)$
16	15	anim2d	$⊢ u = v \to ((x = u \land y = u) \to (x = u \land y = v))$
17	16	2eximdv	$⊢ u = v \to (\exists x \exists y (x = u \land y = u) \to \exists x \exists y (x = u \land y = v))$
18	14 17	syl5com	$⊢ \forall x x = y \to (u = v \to \exists x \exists y (x = u \land y = v))$