Theorem ax6e2eqVD 41248

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 40910) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 40898 is ax6e2eqVD 41248 without virtual deductions and was automatically derived from ax6e2eqVD 41248. (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 40915	. . . . . 6 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥 𝑥 = 𝑦   )
2		ax6ev 1972	. . . . . . . . . 10 ⊢ ∃𝑥 𝑥 = 𝑢
3		hba1 2301	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑥 𝑥 = 𝑦)
4		sp 2182	. . . . . . . . . . . . . 14 ⊢ (∀𝑥∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
5	3, 4	impbii 211	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑥 𝑥 = 𝑦)
6		idn2 40954	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
7		sp 2182	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
8	1, 7	e1a 40968	. . . . . . . . . . . . . . . . . 18 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   𝑥 = 𝑦   )
9		ax7 2023	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑢 → 𝑦 = 𝑢))
10	9	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 → 𝑦 = 𝑢))
11	6, 8, 10	e21 41071	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   𝑦 = 𝑢   )
12		pm3.2 472	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝑦 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
13	6, 11, 12	e22 41012	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥 𝑥 = 𝑦   ,   𝑥 = 𝑢   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
14	13	in2 40946	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
15	14	in1 40912	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
16	15	alimi 1812	. . . . . . . . . . . . 13 ⊢ (∀𝑥∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
17	5, 16	sylbi 219	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
18	1, 17	e1a 40968	. . . . . . . . . . 11 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
19		exim 1834	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) → (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
20	18, 19	e1a 40968	. . . . . . . . . 10 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))   )
21		pm2.27 42	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 = 𝑢 → ((∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
22	2, 20, 21	e01 41032	. . . . . . . . 9 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
23	22	in1 40912	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
24	23	axc4i 2341	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
25	1, 24	e1a 40968	. . . . . 6 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
26		axc11 2452	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
27	1, 25, 26	e11 41029	. . . . 5 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
28		19.2 1981	. . . . 5 ⊢ (∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
29	27, 28	e1a 40968	. . . 4 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
30		excomim 2170	. . . 4 ⊢ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
31	29, 30	e1a 40968	. . 3 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
32		idn1 40915	. . . . . . . . . . 11 ⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
33		idn2 40954	. . . . . . . . . . . 12 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   )
34		simpr 487	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑦 = 𝑢)
35	33, 34	e2 40972	. . . . . . . . . . 11 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑢   )
36		equtrr 2029	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → (𝑦 = 𝑢 → 𝑦 = 𝑣))
37	32, 35, 36	e12 41065	. . . . . . . . . 10 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑦 = 𝑣   )
38		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑢)
39	33, 38	e2 40972	. . . . . . . . . 10 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   𝑥 = 𝑢   )
40		pm3.21 474	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
41	37, 39, 40	e22 41012	. . . . . . . . 9 ⊢ (   𝑢 = 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
42	41	in2 40946	. . . . . . . 8 ⊢ (   𝑢 = 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
43	42	gen11 40957	. . . . . . 7 ⊢ (   𝑢 = 𝑣   ▶   ∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
44		exim 1834	. . . . . . 7 ⊢ (∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
45	43, 44	e1a 40968	. . . . . 6 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
46	45	gen11 40957	. . . . 5 ⊢ (   𝑢 = 𝑣   ▶   ∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
47		exim 1834	. . . . 5 ⊢ (∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
48	46, 47	e1a 40968	. . . 4 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
49	48	in1 40912	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
50		pm2.04 90	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))))
51	50	com12 32	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))))
52	31, 49, 51	e10 41035	. 2 ⊢ (   ∀𝑥 𝑥 = 𝑦   ▶   (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))   )
53	52	in1 40912	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Syntax hints:   → wi 4   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177  ax-13 2390

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-vd1 40911  df-vd2 40919

This theorem is referenced by: (None)