Theorem ax6e2ndeqVD 45850

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

1::	⊢ (   𝑢 ≠ 𝑣   ▶   𝑢 ≠ 𝑣   )
2::	⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
3:2:	⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 = 𝑢   )
4:1,3:	⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑣   )
5:2:	⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑦 = 𝑣   )
6:4,5:	⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑦   )
7::	⊢ (∀𝑥𝑥 = 𝑦 → 𝑥 = 𝑦)
8:7:	⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥𝑥 = 𝑦)
9::	⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
10:8,9:	⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥𝑥 = 𝑦)
11:6,10:	⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶    ¬ ∀𝑥𝑥 = 𝑦   )
12:11:	⊢ (   𝑢 ≠ 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦)   )
13:12:	⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦)   )
14:13:	⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥¬ ∀𝑥𝑥 = 𝑦)   )
15::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥¬ ∀𝑥𝑥 = 𝑦 )
19:15:	⊢ (∃𝑥¬ ∀𝑥𝑥 = 𝑦 ↔ ¬ ∀𝑥𝑥 = 𝑦)
20:14,19:	⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦)   )
21:20:	⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦)   )
22:21:	⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦¬ ∀𝑥𝑥 = 𝑦)   )
23::	⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃ 𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
24:22,23:	⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦¬ ∀𝑥𝑥 = 𝑦)   )
25::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦¬ ∀𝑥𝑥 = 𝑦 )
26:25:	⊢ (∃𝑦¬ ∀𝑥𝑥 = 𝑦 → ∃𝑦∀𝑦¬ ∀𝑥𝑥 = 𝑦)
260::	⊢ (∀𝑦¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦∀𝑦¬ ∀𝑥𝑥 = 𝑦)
27:260:	⊢ (∃𝑦∀𝑦¬ ∀𝑥𝑥 = 𝑦 ↔ ∀𝑦¬ ∀𝑥𝑥 = 𝑦)
270:26,27:	⊢ (∃𝑦¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦¬ ∀𝑥 𝑥 = 𝑦)
28::	⊢ (∀𝑦¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑥𝑥 = 𝑦 )
29:270,28:	⊢ (∃𝑦¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑥𝑥 = 𝑦 )
30:24,29:	⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦)   )
31:30:	⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
32:31:	⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
33::	⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
34:33:	⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣)   )
35:34:	⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
36:35:	⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
37::	⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
38:32,36,37:	⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ( ¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
39::	⊢ (∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦 (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
40::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
41:40:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃ 𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
42::	⊢ (∀𝑥𝑥 = 𝑦 ∨ ¬ ∀𝑥𝑥 = 𝑦)
43:39,41,42:	⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ))
44:40,43:	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥 ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
qed:38,44:	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥 ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Assertion

Ref	Expression
ax6e2ndeqVD	⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

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

Proof of Theorem ax6e2ndeqVD

Step	Hyp	Ref	Expression
1		ax6e2nd 45500	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		ax6e2eq 45499	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
3	1	a1d 26	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
4		exmid 908	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)
5		jao 975	. . . 4 ⊢ ((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))))
6	2, 3, 4, 5	e000 45708	. . 3 ⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
7	1, 6	jaoi 871	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
8		idn1 45516	. . . . . . . . . . . . . . . 16 ⊢ (   𝑢 ≠ 𝑣   ▶   𝑢 ≠ 𝑣   )
9		idn2 45555	. . . . . . . . . . . . . . . . 17 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
10		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
11	9, 10	e2 45573	. . . . . . . . . . . . . . . 16 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 = 𝑢   )
12		neeq1 3018	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝑥 ≠ 𝑣 ↔ 𝑢 ≠ 𝑣))
13	12	biimprcd 253	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ≠ 𝑣 → (𝑥 = 𝑢 → 𝑥 ≠ 𝑣))
14	8, 11, 13	e12 45665	. . . . . . . . . . . . . . 15 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑣   )
15		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
16	9, 15	e2 45573	. . . . . . . . . . . . . . 15 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑦 = 𝑣   )
17		neeq2 3019	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣))
18	17	biimprcd 253	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ≠ 𝑣 → (𝑦 = 𝑣 → 𝑥 ≠ 𝑦))
19	14, 16, 18	e22 45613	. . . . . . . . . . . . . 14 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑦   )
20		df-ne 2957	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
21	20	bicomi 227	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
22		sp 2220	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
23	22	con3i 155	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
24	21, 23	sylbir 238	. . . . . . . . . . . . . 14 ⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
25	19, 24	e2 45573	. . . . . . . . . . . . 13 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶    ¬ ∀𝑥 𝑥 = 𝑦   )
26	25	in2 45547	. . . . . . . . . . . 12 ⊢ (   𝑢 ≠ 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
27	26	gen11 45558	. . . . . . . . . . 11 ⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
28		exim 1867	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
29	27, 28	e1a 45569	. . . . . . . . . 10 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦)   )
30		nfnae 2464	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
31	30	19.9 2242	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
32		imbi2 351	. . . . . . . . . . 11 ⊢ ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
33	32	biimpcd 252	. . . . . . . . . 10 ⊢ ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
34	29, 31, 33	e10 45636	. . . . . . . . 9 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
35	34	gen11 45558	. . . . . . . 8 ⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
36		exim 1867	. . . . . . . 8 ⊢ (∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
37	35, 36	e1a 45569	. . . . . . 7 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
38		excom 2199	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
39		imbi1 350	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
40	39	biimprcd 253	. . . . . . 7 ⊢ ((∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
41	37, 38, 40	e10 45636	. . . . . 6 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
42		hbnae 2462	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
43	42	eximi 1868	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
44		nfa1 2188	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦
45	44	19.9 2242	. . . . . . . 8 ⊢ (∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
46	43, 45	sylib 221	. . . . . . 7 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
47		sp 2220	. . . . . . 7 ⊢ (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
48	46, 47	syl 18	. . . . . 6 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
49		imim1 84	. . . . . 6 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
50	41, 48, 49	e10 45636	. . . . 5 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
51		orc 881	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
52	51	imim2i 17	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
53	50, 52	e1a 45569	. . . 4 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
54	53	in1 45513	. . 3 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
55		idn1 45516	. . . . . 6 ⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
56		ax-1 6	. . . . . 6 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣))
57	55, 56	e1a 45569	. . . . 5 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣)   )
58		olc 882	. . . . . 6 ⊢ (𝑢 = 𝑣 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
59	58	imim2i 17	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
60	57, 59	e1a 45569	. . . 4 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
61	60	in1 45513	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
62		exmidne 2966	. . 3 ⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
63		jao 975	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
64	63	com12 33	. . 3 ⊢ ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
65	54, 61, 62, 64	e000 45708	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
66	7, 65	impbii 212	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2402  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-vd1 45512  df-vd2 45520

This theorem is used by: (None)