Theorem ax6e2eqVD 38165

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 37806) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 37794 is ax6e2eqVD 38165 without virtual deductions and was automatically derived from ax6e2eqVD 38165. (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 37811	. . . . . 6 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥 𝑥 = 𝑦   )
2		ax6ev 1877	. . . . . . . . . 10 ⊢ ∃𝑥 𝑥 = 𝑢
3		hba1 2137	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑥 𝑥 = 𝑦)
4		sp 2041	. . . . . . . . . . . . . 14 ⊢ (∀𝑥∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
5	3, 4	impbii 198	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑥 𝑥 = 𝑦)
6		idn2 37859	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
7		sp 2041	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
8	1, 7	e1a 37873	. . . . . . . . . . . . . . . . . 18 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   𝑥 = 𝑦   )
9		ax7 1930	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑢 → 𝑦 = 𝑢))
10	9	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 → 𝑦 = 𝑢))
11	6, 8, 10	e21 37978	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑦 = 𝑢   )
12		pm3.2 462	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝑦 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
13	6, 11, 12	e22 37917	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
14	13	in2 37851	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
15	14	in1 37808	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
16	15	alimi 1730	. . . . . . . . . . . . 13 ⊢ (∀𝑥∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
17	5, 16	sylbi 206	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
18	1, 17	e1a 37873	. . . . . . . . . . 11 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
19		exim 1751	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) → (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
20	18, 19	e1a 37873	. . . . . . . . . 10 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
21		pm2.27 41	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 = 𝑢 → ((∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
22	2, 20, 21	e01 37937	. . . . . . . . 9 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
23	22	in1 37808	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
24	23	axc4i 2116	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
25	1, 24	e1a 37873	. . . . . 6 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
26		axc11 2302	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
27	1, 25, 26	e11 37934	. . . . 5 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
28		19.2 1879	. . . . 5 ⊢ (∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
29	27, 28	e1a 37873	. . . 4 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
30		excomim 2030	. . . 4 ⊢ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
31	29, 30	e1a 37873	. . 3 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
32		idn1 37811	. . . . . . . . . . 11 ⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
33		idn2 37859	. . . . . . . . . . . 12 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
34		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
35	33, 34	e2 37877	. . . . . . . . . . 11 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑢   )
36		equtrr 1936	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → (𝑦 = 𝑢 → 𝑦 = 𝑣))
37	32, 35, 36	e12 37972	. . . . . . . . . 10 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑣   )
38		simpl 472	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
39	33, 38	e2 37877	. . . . . . . . . 10 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑥 = 𝑢   )
40		pm3.21 463	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
41	37, 39, 40	e22 37917	. . . . . . . . 9 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
42	41	in2 37851	. . . . . . . 8 ⊢ (   𝑢 = 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
43	42	gen11 37862	. . . . . . 7 ⊢ (   𝑢 = 𝑣   ▶   ∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
44		exim 1751	. . . . . . 7 ⊢ (∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
45	43, 44	e1a 37873	. . . . . 6 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
46	45	gen11 37862	. . . . 5 ⊢ (   𝑢 = 𝑣   ▶   ∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
47		exim 1751	. . . . 5 ⊢ (∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
48	46, 47	e1a 37873	. . . 4 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
49	48	in1 37808	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
50		pm2.04 88	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))))
51	50	com12 32	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))))
52	31, 49, 51	e10 37940	. 2 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
53	52	in1 37808	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-vd1 37807  df-vd2 37815

This theorem is referenced by: (None)