Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  euoreqb Structured version   Visualization version   GIF version

Theorem euoreqb 43604
 Description: There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023.)
Assertion
Ref Expression
euoreqb ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑉

Proof of Theorem euoreqb
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2826 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
2 eqeq1 2826 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐵𝑦 = 𝐵))
31, 2orbi12d 916 . . . 4 (𝑥 = 𝑦 → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑦 = 𝐴𝑦 = 𝐵)))
43reu8 3699 . . 3 (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)))
5 simprlr 779 . . . . . . . . . 10 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐵𝑉)
6 eqeq1 2826 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐴𝐵 = 𝐴))
7 eqeq1 2826 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐵𝐵 = 𝐵))
86, 7orbi12d 916 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐵 = 𝐴𝐵 = 𝐵)))
9 eqeq2 2834 . . . . . . . . . . . 12 (𝑦 = 𝐵 → (𝑥 = 𝑦𝑥 = 𝐵))
108, 9imbi12d 348 . . . . . . . . . . 11 (𝑦 = 𝐵 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
1110rspcv 3593 . . . . . . . . . 10 (𝐵𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
125, 11syl 17 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
13 ioran 981 . . . . . . . . . . . 12 (¬ (𝐵 = 𝐴𝐵 = 𝐵) ↔ (¬ 𝐵 = 𝐴 ∧ ¬ 𝐵 = 𝐵))
14 eqid 2822 . . . . . . . . . . . . 13 𝐵 = 𝐵
1514pm2.24i 153 . . . . . . . . . . . 12 𝐵 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
1613, 15simplbiim 508 . . . . . . . . . . 11 (¬ (𝐵 = 𝐴𝐵 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
17 eqtr2 2843 . . . . . . . . . . . . . 14 ((𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵)
1817ancoms 462 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐴 = 𝐵)
1918a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐵𝑥 = 𝐴) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
2019expimpd 457 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2116, 20ja 189 . . . . . . . . . 10 (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2221com12 32 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → 𝐴 = 𝐵))
2312, 22syld 47 . . . . . . . 8 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
2423ex 416 . . . . . . 7 (𝑥 = 𝐴 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
25 simprll 778 . . . . . . . . . 10 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴𝑉)
26 eqeq1 2826 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐴𝐴 = 𝐴))
27 eqeq1 2826 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐵𝐴 = 𝐵))
2826, 27orbi12d 916 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
29 eqeq2 2834 . . . . . . . . . . . 12 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
3028, 29imbi12d 348 . . . . . . . . . . 11 (𝑦 = 𝐴 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3130rspcv 3593 . . . . . . . . . 10 (𝐴𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3225, 31syl 17 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
33 ioran 981 . . . . . . . . . . . 12 (¬ (𝐴 = 𝐴𝐴 = 𝐵) ↔ (¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵))
34 eqid 2822 . . . . . . . . . . . . . 14 𝐴 = 𝐴
3534pm2.24i 153 . . . . . . . . . . . . 13 𝐴 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3635adantr 484 . . . . . . . . . . . 12 ((¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3733, 36sylbi 220 . . . . . . . . . . 11 (¬ (𝐴 = 𝐴𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3817a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
3938expimpd 457 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4037, 39ja 189 . . . . . . . . . 10 (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4140com12 32 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → 𝐴 = 𝐵))
4232, 41syld 47 . . . . . . . 8 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
4342ex 416 . . . . . . 7 (𝑥 = 𝐵 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4424, 43jaoi 854 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4544com12 32 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → ((𝑥 = 𝐴𝑥 = 𝐵) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4645impd 414 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
4746rexlimdva 3270 . . 3 ((𝐴𝑉𝐵𝑉) → (∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
484, 47syl5bi 245 . 2 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵))
49 reueq 3703 . . . . . . 7 (𝐵𝑉 ↔ ∃!𝑥𝑉 𝑥 = 𝐵)
5049biimpi 219 . . . . . 6 (𝐵𝑉 → ∃!𝑥𝑉 𝑥 = 𝐵)
5150adantl 485 . . . . 5 ((𝐴𝑉𝐵𝑉) → ∃!𝑥𝑉 𝑥 = 𝐵)
5251adantr 484 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 𝑥 = 𝐵)
53 eqeq2 2834 . . . . . . . 8 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
5453adantl 485 . . . . . . 7 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (𝑥 = 𝐴𝑥 = 𝐵))
5554orbi1d 914 . . . . . 6 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑥 = 𝐵𝑥 = 𝐵)))
56 oridm 902 . . . . . 6 ((𝑥 = 𝐵𝑥 = 𝐵) ↔ 𝑥 = 𝐵)
5755, 56syl6bb 290 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝑥 = 𝐵))
5857reubidv 3370 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃!𝑥𝑉 𝑥 = 𝐵))
5952, 58mpbird 260 . . 3 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵))
6059ex 416 . 2 ((𝐴𝑉𝐵𝑉) → (𝐴 = 𝐵 → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵)))
6148, 60impbid 215 1 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2114  ∀wral 3130  ∃wrex 3131  ∃!wreu 3132 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-cleq 2815  df-clel 2894  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138 This theorem is referenced by:  quad1  44077  requad1  44079
 Copyright terms: Public domain W3C validator