Users' Mathboxes 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 44552
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 2743 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
2 eqeq1 2743 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐵𝑦 = 𝐵))
31, 2orbi12d 915 . . . 4 (𝑥 = 𝑦 → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑦 = 𝐴𝑦 = 𝐵)))
43reu8 3671 . . 3 (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)))
5 simprlr 776 . . . . . . . . . 10 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐵𝑉)
6 eqeq1 2743 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐴𝐵 = 𝐴))
7 eqeq1 2743 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐵𝐵 = 𝐵))
86, 7orbi12d 915 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐵 = 𝐴𝐵 = 𝐵)))
9 eqeq2 2751 . . . . . . . . . . . 12 (𝑦 = 𝐵 → (𝑥 = 𝑦𝑥 = 𝐵))
108, 9imbi12d 344 . . . . . . . . . . 11 (𝑦 = 𝐵 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
1110rspcv 3555 . . . . . . . . . 10 (𝐵𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
125, 11syl 17 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
13 ioran 980 . . . . . . . . . . . 12 (¬ (𝐵 = 𝐴𝐵 = 𝐵) ↔ (¬ 𝐵 = 𝐴 ∧ ¬ 𝐵 = 𝐵))
14 eqid 2739 . . . . . . . . . . . . 13 𝐵 = 𝐵
1514pm2.24i 150 . . . . . . . . . . . 12 𝐵 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
1613, 15simplbiim 504 . . . . . . . . . . 11 (¬ (𝐵 = 𝐴𝐵 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
17 eqtr2 2763 . . . . . . . . . . . . . 14 ((𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵)
1817ancoms 458 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐴 = 𝐵)
1918a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐵𝑥 = 𝐴) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
2019expimpd 453 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2116, 20ja 186 . . . . . . . . . 10 (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2221com12 32 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → 𝐴 = 𝐵))
2312, 22syld 47 . . . . . . . 8 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
2423ex 412 . . . . . . 7 (𝑥 = 𝐴 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
25 simprll 775 . . . . . . . . . 10 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴𝑉)
26 eqeq1 2743 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐴𝐴 = 𝐴))
27 eqeq1 2743 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐵𝐴 = 𝐵))
2826, 27orbi12d 915 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
29 eqeq2 2751 . . . . . . . . . . . 12 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
3028, 29imbi12d 344 . . . . . . . . . . 11 (𝑦 = 𝐴 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3130rspcv 3555 . . . . . . . . . 10 (𝐴𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3225, 31syl 17 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
33 ioran 980 . . . . . . . . . . . 12 (¬ (𝐴 = 𝐴𝐴 = 𝐵) ↔ (¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵))
34 eqid 2739 . . . . . . . . . . . . . 14 𝐴 = 𝐴
3534pm2.24i 150 . . . . . . . . . . . . 13 𝐴 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3635adantr 480 . . . . . . . . . . . 12 ((¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3733, 36sylbi 216 . . . . . . . . . . 11 (¬ (𝐴 = 𝐴𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3817a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
3938expimpd 453 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4037, 39ja 186 . . . . . . . . . 10 (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4140com12 32 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → 𝐴 = 𝐵))
4232, 41syld 47 . . . . . . . 8 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
4342ex 412 . . . . . . 7 (𝑥 = 𝐵 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4424, 43jaoi 853 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4544com12 32 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → ((𝑥 = 𝐴𝑥 = 𝐵) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4645impd 410 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
4746rexlimdva 3214 . . 3 ((𝐴𝑉𝐵𝑉) → (∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
484, 47syl5bi 241 . 2 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵))
49 reueq 3675 . . . . . . 7 (𝐵𝑉 ↔ ∃!𝑥𝑉 𝑥 = 𝐵)
5049biimpi 215 . . . . . 6 (𝐵𝑉 → ∃!𝑥𝑉 𝑥 = 𝐵)
5150adantl 481 . . . . 5 ((𝐴𝑉𝐵𝑉) → ∃!𝑥𝑉 𝑥 = 𝐵)
5251adantr 480 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 𝑥 = 𝐵)
53 eqeq2 2751 . . . . . . . 8 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
5453adantl 481 . . . . . . 7 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (𝑥 = 𝐴𝑥 = 𝐵))
5554orbi1d 913 . . . . . 6 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑥 = 𝐵𝑥 = 𝐵)))
56 oridm 901 . . . . . 6 ((𝑥 = 𝐵𝑥 = 𝐵) ↔ 𝑥 = 𝐵)
5755, 56bitrdi 286 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝑥 = 𝐵))
5857reubidv 3321 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃!𝑥𝑉 𝑥 = 𝐵))
5952, 58mpbird 256 . . 3 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵))
6059ex 412 . 2 ((𝐴𝑉𝐵𝑉) → (𝐴 = 𝐵 → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵)))
6148, 60impbid 211 1 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843   = wceq 1541  wcel 2109  wral 3065  wrex 3066  ∃!wreu 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-12 2174  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073
This theorem is referenced by:  quad1  45024  requad1  45026
  Copyright terms: Public domain W3C validator