Theorem ax6e2ndeqVD 38167

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 ax6e2ndeqVD 38167 without virtual deductions and was automatically derived from ax6e2ndeqVD 38167. (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 37795	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		ax6e2eq 37794	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
3	1	a1d 25	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
4		exmid 430	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)
5		jao 533	. . . 4 ⊢ ((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))))
6	2, 3, 4, 5	e000 38015	. . 3 ⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
7	1, 6	jaoi 393	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
8		idn1 37811	. . . . . . . . . . . . . . . 16 ⊢ (   𝑢 ≠ 𝑣   ▶   𝑢 ≠ 𝑣   )
9		idn2 37859	. . . . . . . . . . . . . . . . 17 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
10		simpl 472	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
11	9, 10	e2 37877	. . . . . . . . . . . . . . . 16 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 = 𝑢   )
12		neeq1 2844	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝑥 ≠ 𝑣 ↔ 𝑢 ≠ 𝑣))
13	12	biimprcd 239	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ≠ 𝑣 → (𝑥 = 𝑢 → 𝑥 ≠ 𝑣))
14	8, 11, 13	e12 37972	. . . . . . . . . . . . . . 15 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑣   )
15		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
16	9, 15	e2 37877	. . . . . . . . . . . . . . 15 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑦 = 𝑣   )
17		neeq2 2845	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣))
18	17	biimprcd 239	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ≠ 𝑣 → (𝑦 = 𝑣 → 𝑥 ≠ 𝑦))
19	14, 16, 18	e22 37917	. . . . . . . . . . . . . 14 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑦   )
20		df-ne 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
21	20	bicomi 213	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
22		sp 2041	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
23	22	con3i 149	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
24	21, 23	sylbir 224	. . . . . . . . . . . . . 14 ⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
25	19, 24	e2 37877	. . . . . . . . . . . . 13 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶    ¬ ∀𝑥 𝑥 = 𝑦   )
26	25	in2 37851	. . . . . . . . . . . 12 ⊢ (   𝑢 ≠ 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
27	26	gen11 37862	. . . . . . . . . . 11 ⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
28		exim 1751	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
29	27, 28	e1a 37873	. . . . . . . . . 10 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦)   )
30		nfnae 2306	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
31	30	19.9 2060	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
32		imbi2 337	. . . . . . . . . . 11 ⊢ ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
33	32	biimpcd 238	. . . . . . . . . 10 ⊢ ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
34	29, 31, 33	e10 37940	. . . . . . . . 9 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
35	34	gen11 37862	. . . . . . . 8 ⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
36		exim 1751	. . . . . . . 8 ⊢ (∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
37	35, 36	e1a 37873	. . . . . . 7 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
38		excom 2029	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
39		imbi1 336	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
40	39	biimprcd 239	. . . . . . 7 ⊢ ((∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
41	37, 38, 40	e10 37940	. . . . . 6 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
42		hbnae 2305	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
43	42	eximi 1752	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
44		nfa1 2015	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦
45	44	19.9 2060	. . . . . . . 8 ⊢ (∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
46	43, 45	sylib 207	. . . . . . 7 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
47		sp 2041	. . . . . . 7 ⊢ (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
48	46, 47	syl 17	. . . . . 6 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
49		imim1 81	. . . . . 6 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
50	41, 48, 49	e10 37940	. . . . 5 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
51		orc 399	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
52	51	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
53	50, 52	e1a 37873	. . . 4 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
54	53	in1 37808	. . 3 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
55		idn1 37811	. . . . . 6 ⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
56		ax-1 6	. . . . . 6 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣))
57	55, 56	e1a 37873	. . . . 5 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣)   )
58		olc 398	. . . . . 6 ⊢ (𝑢 = 𝑣 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
59	58	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
60	57, 59	e1a 37873	. . . 4 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
61	60	in1 37808	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
62		exmidne 2792	. . 3 ⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
63		jao 533	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
64	63	com12 32	. . 3 ⊢ ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
65	54, 61, 62, 64	e000 38015	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
66	7, 65	impbii 198	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ≠ wne 2780

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  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ne 2782  df-v 3175  df-vd1 37807  df-vd2 37815

This theorem is referenced by: (None)