Theorem ax6e2eqVD 39143

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

1::	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∀𝑥𝑥 = 𝑦   )
2::	⊢ (   ∀𝑥𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
3:1:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   𝑥 = 𝑦   )
4:2,3:	⊢ (   ∀𝑥𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑦 = 𝑢   )
5:2,4:	⊢ (   ∀𝑥𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
6:5:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
7:6:	⊢ (∀𝑥𝑥 = 𝑦 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
8:7:	⊢ (∀𝑥∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
9::	⊢ (∀𝑥𝑥 = 𝑦 ↔ ∀𝑥∀𝑥𝑥 = 𝑦)
10:8,9:	⊢ (∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
11:1,10:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
12:11:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   (∃𝑥𝑥 = 𝑢 → ∃𝑥 (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
13::	⊢ ∃𝑥𝑥 = 𝑢
14:13,12:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )   )
140:14:	⊢ (∀𝑥𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
141:140:	⊢ (∀𝑥𝑥 = 𝑦 → ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
15:1,141:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
16:1,15:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
17:16:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
18:17:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
19::	⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
20::	⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
21:20:	⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑢    )
22:19,21:	⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑣    )
23:20:	⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑥 = 𝑢    )
24:22,23:	⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
25:24:	⊢ (   𝑢 = 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
26:25:	⊢ (   𝑢 = 𝑣   ▶   ∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
27:26:	⊢ (   𝑢 = 𝑣   ▶   (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
28:27:	⊢ (   𝑢 = 𝑣   ▶   ∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
29:28:	⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
30:29:	⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
31:18,30:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   (𝑢 = 𝑣 → ∃𝑥∃𝑦 (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
qed:31:	⊢ (∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Assertion

Ref	Expression
ax6e2eqVD	⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣   𝑦,𝑣

Proof of Theorem ax6e2eqVD

Step	Hyp	Ref	Expression
1		idn1 38790	. . . . . 6 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥 𝑥 = 𝑦   )
2		ax6ev 1890	. . . . . . . . . 10 ⊢ ∃𝑥 𝑥 = 𝑢
3		hba1 2151	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑥 𝑥 = 𝑦)
4		sp 2053	. . . . . . . . . . . . . 14 ⊢ (∀𝑥∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
5	3, 4	impbii 199	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑥 𝑥 = 𝑦)
6		idn2 38838	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
7		sp 2053	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
8	1, 7	e1a 38852	. . . . . . . . . . . . . . . . . 18 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   𝑥 = 𝑦   )
9		ax7 1943	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑢 → 𝑦 = 𝑢))
10	9	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 → 𝑦 = 𝑢))
11	6, 8, 10	e21 38957	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑦 = 𝑢   )
12		pm3.2 463	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝑦 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
13	6, 11, 12	e22 38896	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
14	13	in2 38830	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
15	14	in1 38787	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
16	15	alimi 1739	. . . . . . . . . . . . 13 ⊢ (∀𝑥∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
17	5, 16	sylbi 207	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
18	1, 17	e1a 38852	. . . . . . . . . . 11 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
19		exim 1761	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) → (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
20	18, 19	e1a 38852	. . . . . . . . . 10 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
21		pm2.27 42	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 = 𝑢 → ((∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
22	2, 20, 21	e01 38916	. . . . . . . . 9 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
23	22	in1 38787	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
24	23	axc4i 2131	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
25	1, 24	e1a 38852	. . . . . 6 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
26		axc11 2314	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
27	1, 25, 26	e11 38913	. . . . 5 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
28		19.2 1892	. . . . 5 ⊢ (∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
29	27, 28	e1a 38852	. . . 4 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
30		excomim 2043	. . . 4 ⊢ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
31	29, 30	e1a 38852	. . 3 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
32		idn1 38790	. . . . . . . . . . 11 ⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
33		idn2 38838	. . . . . . . . . . . 12 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
34		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
35	33, 34	e2 38856	. . . . . . . . . . 11 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑢   )
36		equtrr 1949	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → (𝑦 = 𝑢 → 𝑦 = 𝑣))
37	32, 35, 36	e12 38951	. . . . . . . . . 10 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑣   )
38		simpl 473	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
39	33, 38	e2 38856	. . . . . . . . . 10 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑥 = 𝑢   )
40		pm3.21 464	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
41	37, 39, 40	e22 38896	. . . . . . . . 9 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
42	41	in2 38830	. . . . . . . 8 ⊢ (   𝑢 = 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
43	42	gen11 38841	. . . . . . 7 ⊢ (   𝑢 = 𝑣   ▶   ∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
44		exim 1761	. . . . . . 7 ⊢ (∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
45	43, 44	e1a 38852	. . . . . 6 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
46	45	gen11 38841	. . . . 5 ⊢ (   𝑢 = 𝑣   ▶   ∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
47		exim 1761	. . . . 5 ⊢ (∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
48	46, 47	e1a 38852	. . . 4 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
49	48	in1 38787	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
50		pm2.04 90	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))))
51	50	com12 32	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))))
52	31, 49, 51	e10 38919	. 2 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
53	52	in1 38787	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1481   = wceq 1483  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-vd1 38786  df-vd2 38794

This theorem is referenced by: (None)