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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑢
2		hbae	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 )
3		ax7	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → 𝑦 = 𝑢 ) )
4	3	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → 𝑦 = 𝑢 ) )
5	4	ancld	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
6	2 5	eximdh	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝑥 = 𝑢 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
7	1 6	mpi	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
8	7	axc4i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
9		axc11	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
10	8 9	mpd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
11		19.2	⊢ ( ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
12	10 11	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
13		excomim	⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
14	12 13	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
15		equtrr	⊢ ( 𝑢 = 𝑣 → ( 𝑦 = 𝑢 → 𝑦 = 𝑣 ) )
16	15	anim2d	⊢ ( 𝑢 = 𝑣 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
17	16	2eximdv	⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
18	14 17	syl5com	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )