Theorem ax6e2ndeqVD 42154

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 41814) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 41802 is ax6e2ndeqVD 42154 without virtual deductions and was automatically derived from ax6e2ndeqVD 42154. (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 41803	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		ax6e2eq 41802	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
3	1	a1d 25	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
4		exmid 895	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)
5		jao 961	. . . 4 ⊢ ((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) → ((∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))))
6	2, 3, 4, 5	e000 42012	. . 3 ⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
7	1, 6	jaoi 857	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
8		idn1 41819	. . . . . . . . . . . . . . . 16 ⊢ (   𝑢 ≠ 𝑣   ▶   𝑢 ≠ 𝑣   )
9		idn2 41858	. . . . . . . . . . . . . . . . 17 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
10		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
11	9, 10	e2 41876	. . . . . . . . . . . . . . . 16 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 = 𝑢   )
12		neeq1 2997	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝑥 ≠ 𝑣 ↔ 𝑢 ≠ 𝑣))
13	12	biimprcd 253	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ≠ 𝑣 → (𝑥 = 𝑢 → 𝑥 ≠ 𝑣))
14	8, 11, 13	e12 41969	. . . . . . . . . . . . . . 15 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑣   )
15		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
16	9, 15	e2 41876	. . . . . . . . . . . . . . 15 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑦 = 𝑣   )
17		neeq2 2998	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → (𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣))
18	17	biimprcd 253	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ≠ 𝑣 → (𝑦 = 𝑣 → 𝑥 ≠ 𝑦))
19	14, 16, 18	e22 41916	. . . . . . . . . . . . . 14 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶   𝑥 ≠ 𝑦   )
20		df-ne 2936	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦)
21	20	bicomi 227	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
22		sp 2180	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
23	22	con3i 157	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
24	21, 23	sylbir 238	. . . . . . . . . . . . . 14 ⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
25	19, 24	e2 41876	. . . . . . . . . . . . 13 ⊢ (   𝑢 ≠ 𝑣   ,   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ▶    ¬ ∀𝑥 𝑥 = 𝑦   )
26	25	in2 41850	. . . . . . . . . . . 12 ⊢ (   𝑢 ≠ 𝑣   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
27	26	gen11 41861	. . . . . . . . . . 11 ⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
28		exim 1841	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
29	27, 28	e1a 41872	. . . . . . . . . 10 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦)   )
30		nfnae 2431	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
31	30	19.9 2203	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
32		imbi2 352	. . . . . . . . . . 11 ⊢ ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
33	32	biimpcd 252	. . . . . . . . . 10 ⊢ ((∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
34	29, 31, 33	e10 41939	. . . . . . . . 9 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
35	34	gen11 41861	. . . . . . . 8 ⊢ (   𝑢 ≠ 𝑣   ▶   ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
36		exim 1841	. . . . . . . 8 ⊢ (∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
37	35, 36	e1a 41872	. . . . . . 7 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
38		excom 2166	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
39		imbi1 351	. . . . . . . 8 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
40	39	biimprcd 253	. . . . . . 7 ⊢ ((∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
41	37, 38, 40	e10 41939	. . . . . 6 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
42		hbnae 2429	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
43	42	eximi 1842	. . . . . . . 8 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
44		nfa1 2152	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦
45	44	19.9 2203	. . . . . . . 8 ⊢ (∃𝑦∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
46	43, 45	sylib 221	. . . . . . 7 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
47		sp 2180	. . . . . . 7 ⊢ (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
48	46, 47	syl 17	. . . . . 6 ⊢ (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
49		imim1 83	. . . . . 6 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
50	41, 48, 49	e10 41939	. . . . 5 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
51		orc 867	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
52	51	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
53	50, 52	e1a 41872	. . . 4 ⊢ (   𝑢 ≠ 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
54	53	in1 41816	. . 3 ⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
55		idn1 41819	. . . . . 6 ⊢ (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
56		ax-1 6	. . . . . 6 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣))
57	55, 56	e1a 41872	. . . . 5 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣)   )
58		olc 868	. . . . . 6 ⊢ (𝑢 = 𝑣 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
59	58	imim2i 16	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
60	57, 59	e1a 41872	. . . 4 ⊢ (   𝑢 = 𝑣   ▶   (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))   )
61	60	in1 41816	. . 3 ⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
62		exmidne 2945	. . 3 ⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
63		jao 961	. . . 4 ⊢ ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
64	63	com12 32	. . 3 ⊢ ((𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))) → ((𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣) → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))))
65	54, 61, 62, 64	e000 42012	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
66	7, 65	impbii 212	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847  ∀wal 1541   = wceq 1543  ∃wex 1787   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-13 2369  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2713  df-cleq 2726  df-clel 2812  df-ne 2936  df-v 3403  df-vd1 41815  df-vd2 41823

This theorem is referenced by: (None)