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 42715
 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 2782 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
2 eqeq1 2782 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐵𝑦 = 𝐵))
31, 2orbi12d 902 . . . 4 (𝑥 = 𝑦 → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑦 = 𝐴𝑦 = 𝐵)))
43reu8 3638 . . 3 (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)))
5 simprlr 767 . . . . . . . . . 10 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐵𝑉)
6 eqeq1 2782 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐴𝐵 = 𝐴))
7 eqeq1 2782 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐵𝐵 = 𝐵))
86, 7orbi12d 902 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐵 = 𝐴𝐵 = 𝐵)))
9 eqeq2 2789 . . . . . . . . . . . 12 (𝑦 = 𝐵 → (𝑥 = 𝑦𝑥 = 𝐵))
108, 9imbi12d 337 . . . . . . . . . . 11 (𝑦 = 𝐵 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
1110rspcv 3531 . . . . . . . . . 10 (𝐵𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
125, 11syl 17 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
13 ioran 966 . . . . . . . . . . . 12 (¬ (𝐵 = 𝐴𝐵 = 𝐵) ↔ (¬ 𝐵 = 𝐴 ∧ ¬ 𝐵 = 𝐵))
14 eqid 2778 . . . . . . . . . . . . 13 𝐵 = 𝐵
1514pm2.24i 148 . . . . . . . . . . . 12 𝐵 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
1613, 15simplbiim 497 . . . . . . . . . . 11 (¬ (𝐵 = 𝐴𝐵 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
17 eqtr2 2800 . . . . . . . . . . . . . 14 ((𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵)
1817ancoms 451 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐴 = 𝐵)
1918a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐵𝑥 = 𝐴) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
2019expimpd 446 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2116, 20ja 175 . . . . . . . . . 10 (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2221com12 32 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → 𝐴 = 𝐵))
2312, 22syld 47 . . . . . . . 8 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
2423ex 405 . . . . . . 7 (𝑥 = 𝐴 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
25 simprll 766 . . . . . . . . . 10 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴𝑉)
26 eqeq1 2782 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐴𝐴 = 𝐴))
27 eqeq1 2782 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐵𝐴 = 𝐵))
2826, 27orbi12d 902 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
29 eqeq2 2789 . . . . . . . . . . . 12 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
3028, 29imbi12d 337 . . . . . . . . . . 11 (𝑦 = 𝐴 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3130rspcv 3531 . . . . . . . . . 10 (𝐴𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3225, 31syl 17 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
33 ioran 966 . . . . . . . . . . . 12 (¬ (𝐴 = 𝐴𝐴 = 𝐵) ↔ (¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵))
34 eqid 2778 . . . . . . . . . . . . . 14 𝐴 = 𝐴
3534pm2.24i 148 . . . . . . . . . . . . 13 𝐴 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3635adantr 473 . . . . . . . . . . . 12 ((¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3733, 36sylbi 209 . . . . . . . . . . 11 (¬ (𝐴 = 𝐴𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3817a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
3938expimpd 446 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4037, 39ja 175 . . . . . . . . . 10 (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4140com12 32 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → 𝐴 = 𝐵))
4232, 41syld 47 . . . . . . . 8 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
4342ex 405 . . . . . . 7 (𝑥 = 𝐵 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4424, 43jaoi 843 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4544com12 32 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → ((𝑥 = 𝐴𝑥 = 𝐵) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4645impd 402 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
4746rexlimdva 3229 . . 3 ((𝐴𝑉𝐵𝑉) → (∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
484, 47syl5bi 234 . 2 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵))
49 reueq 3642 . . . . . . 7 (𝐵𝑉 ↔ ∃!𝑥𝑉 𝑥 = 𝐵)
5049biimpi 208 . . . . . 6 (𝐵𝑉 → ∃!𝑥𝑉 𝑥 = 𝐵)
5150adantl 474 . . . . 5 ((𝐴𝑉𝐵𝑉) → ∃!𝑥𝑉 𝑥 = 𝐵)
5251adantr 473 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 𝑥 = 𝐵)
53 eqeq2 2789 . . . . . . . 8 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
5453adantl 474 . . . . . . 7 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (𝑥 = 𝐴𝑥 = 𝐵))
5554orbi1d 900 . . . . . 6 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑥 = 𝐵𝑥 = 𝐵)))
56 oridm 888 . . . . . 6 ((𝑥 = 𝐵𝑥 = 𝐵) ↔ 𝑥 = 𝐵)
5755, 56syl6bb 279 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝑥 = 𝐵))
5857reubidv 3329 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃!𝑥𝑉 𝑥 = 𝐵))
5952, 58mpbird 249 . . 3 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵))
6059ex 405 . 2 ((𝐴𝑉𝐵𝑉) → (𝐴 = 𝐵 → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵)))
6148, 60impbid 204 1 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∨ wo 833   = wceq 1507   ∈ wcel 2050  ∀wral 3088  ∃wrex 3089  ∃!wreu 3090 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-v 3417 This theorem is referenced by:  quad1  43154  requad1  43156
 Copyright terms: Public domain W3C validator