Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax6e2ndeqVD Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ax6e2nd 37795 . . 3 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
2 ax6e2eq 37794 . . . 4 (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)))
31a1d 25 . . . 4 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)))
4 exmid 430 . . . 4 (∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦)
5 jao 533 . . . 4 ((∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))) → ((¬ ∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))) → ((∀𝑥 𝑥 = 𝑦 ∨ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)))))
62, 3, 4, 5e000 38015 . . 3 (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
71, 6jaoi 393 . 2 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
8 idn1 37811 . . . . . . . . . . . . . . . 16 (   𝑢𝑣   ▶   𝑢𝑣   )
9 idn2 37859 . . . . . . . . . . . . . . . . 17 (   𝑢𝑣   ,   (𝑥 = 𝑢𝑦 = 𝑣)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
10 simpl 472 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
119, 10e2 37877 . . . . . . . . . . . . . . . 16 (   𝑢𝑣   ,   (𝑥 = 𝑢𝑦 = 𝑣)   ▶   𝑥 = 𝑢   )
12 neeq1 2844 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → (𝑥𝑣𝑢𝑣))
1312biimprcd 239 . . . . . . . . . . . . . . . 16 (𝑢𝑣 → (𝑥 = 𝑢𝑥𝑣))
148, 11, 13e12 37972 . . . . . . . . . . . . . . 15 (   𝑢𝑣   ,   (𝑥 = 𝑢𝑦 = 𝑣)   ▶   𝑥𝑣   )
15 simpr 476 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
169, 15e2 37877 . . . . . . . . . . . . . . 15 (   𝑢𝑣   ,   (𝑥 = 𝑢𝑦 = 𝑣)   ▶   𝑦 = 𝑣   )
17 neeq2 2845 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → (𝑥𝑦𝑥𝑣))
1817biimprcd 239 . . . . . . . . . . . . . . 15 (𝑥𝑣 → (𝑦 = 𝑣𝑥𝑦))
1914, 16, 18e22 37917 . . . . . . . . . . . . . 14 (   𝑢𝑣   ,   (𝑥 = 𝑢𝑦 = 𝑣)   ▶   𝑥𝑦   )
20 df-ne 2782 . . . . . . . . . . . . . . . 16 (𝑥𝑦 ↔ ¬ 𝑥 = 𝑦)
2120bicomi 213 . . . . . . . . . . . . . . 15 𝑥 = 𝑦𝑥𝑦)
22 sp 2041 . . . . . . . . . . . . . . . 16 (∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)
2322con3i 149 . . . . . . . . . . . . . . 15 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
2421, 23sylbir 224 . . . . . . . . . . . . . 14 (𝑥𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
2519, 24e2 37877 . . . . . . . . . . . . 13 (   𝑢𝑣   ,   (𝑥 = 𝑢𝑦 = 𝑣)   ▶    ¬ ∀𝑥 𝑥 = 𝑦   )
2625in2 37851 . . . . . . . . . . . 12 (   𝑢𝑣   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
2726gen11 37862 . . . . . . . . . . 11 (   𝑢𝑣   ▶   𝑥((𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
28 exim 1751 . . . . . . . . . . 11 (∀𝑥((𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦))
2927, 28e1a 37873 . . . . . . . . . 10 (   𝑢𝑣   ▶   (∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦)   )
30 nfnae 2306 . . . . . . . . . . 11 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
313019.9 2060 . . . . . . . . . 10 (∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
32 imbi2 337 . . . . . . . . . . 11 ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
3332biimpcd 238 . . . . . . . . . 10 ((∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
3429, 31, 33e10 37940 . . . . . . . . 9 (   𝑢𝑣   ▶   (∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
3534gen11 37862 . . . . . . . 8 (   𝑢𝑣   ▶   𝑦(∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
36 exim 1751 . . . . . . . 8 (∀𝑦(∃𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦))
3735, 36e1a 37873 . . . . . . 7 (   𝑢𝑣   ▶   (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
38 excom 2029 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ↔ ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
39 imbi1 336 . . . . . . . 8 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ↔ ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) ↔ (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
4039biimprcd 239 . . . . . . 7 ((∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ↔ ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)))
4137, 38, 40e10 37940 . . . . . 6 (   𝑢𝑣   ▶   (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦)   )
42 hbnae 2305 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
4342eximi 1752 . . . . . . . 8 (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
44 nfa1 2015 . . . . . . . . 9 𝑦𝑦 ¬ ∀𝑥 𝑥 = 𝑦
454419.9 2060 . . . . . . . 8 (∃𝑦𝑦 ¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
4643, 45sylib 207 . . . . . . 7 (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
47 sp 2041 . . . . . . 7 (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
4846, 47syl 17 . . . . . 6 (∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
49 imim1 81 . . . . . 6 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦) → ((∃𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)))
5041, 48, 49e10 37940 . . . . 5 (   𝑢𝑣   ▶   (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦)   )
51 orc 399 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))
5251imim2i 16 . . . . 5 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)))
5350, 52e1a 37873 . . . 4 (   𝑢𝑣   ▶   (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))   )
5453in1 37808 . . 3 (𝑢𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)))
55 idn1 37811 . . . . . 6 (   𝑢 = 𝑣   ▶   𝑢 = 𝑣   )
56 ax-1 6 . . . . . 6 (𝑢 = 𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → 𝑢 = 𝑣))
5755, 56e1a 37873 . . . . 5 (   𝑢 = 𝑣   ▶   (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → 𝑢 = 𝑣)   )
58 olc 398 . . . . . 6 (𝑢 = 𝑣 → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))
5958imim2i 16 . . . . 5 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → 𝑢 = 𝑣) → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)))
6057, 59e1a 37873 . . . 4 (   𝑢 = 𝑣   ▶   (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))   )
6160in1 37808 . . 3 (𝑢 = 𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)))
62 exmidne 2792 . . 3 (𝑢 = 𝑣𝑢𝑣)
63 jao 533 . . . 4 ((𝑢 = 𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))) → ((𝑢𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))) → ((𝑢 = 𝑣𝑢𝑣) → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)))))
6463com12 32 . . 3 ((𝑢𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))) → ((𝑢 = 𝑣 → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))) → ((𝑢 = 𝑣𝑢𝑣) → (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)))))
6554, 61, 62, 64e000 38015 . 2 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))
667, 65impbii 198 1 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
 Colors of variables: wff setvar class 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)
 Copyright terms: Public domain W3C validator