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 44601
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 2742 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
2 eqeq1 2742 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝐵𝑦 = 𝐵))
31, 2orbi12d 916 . . . 4 (𝑥 = 𝑦 → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑦 = 𝐴𝑦 = 𝐵)))
43reu8 3668 . . 3 (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)))
5 simprlr 777 . . . . . . . . . 10 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐵𝑉)
6 eqeq1 2742 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐴𝐵 = 𝐴))
7 eqeq1 2742 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑦 = 𝐵𝐵 = 𝐵))
86, 7orbi12d 916 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐵 = 𝐴𝐵 = 𝐵)))
9 eqeq2 2750 . . . . . . . . . . . 12 (𝑦 = 𝐵 → (𝑥 = 𝑦𝑥 = 𝐵))
108, 9imbi12d 345 . . . . . . . . . . 11 (𝑦 = 𝐵 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
1110rspcv 3557 . . . . . . . . . 10 (𝐵𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
125, 11syl 17 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵)))
13 ioran 981 . . . . . . . . . . . 12 (¬ (𝐵 = 𝐴𝐵 = 𝐵) ↔ (¬ 𝐵 = 𝐴 ∧ ¬ 𝐵 = 𝐵))
14 eqid 2738 . . . . . . . . . . . . 13 𝐵 = 𝐵
1514pm2.24i 150 . . . . . . . . . . . 12 𝐵 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
1613, 15simplbiim 505 . . . . . . . . . . 11 (¬ (𝐵 = 𝐴𝐵 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
17 eqtr2 2762 . . . . . . . . . . . . . 14 ((𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵)
1817ancoms 459 . . . . . . . . . . . . 13 ((𝑥 = 𝐵𝑥 = 𝐴) → 𝐴 = 𝐵)
1918a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐵𝑥 = 𝐴) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
2019expimpd 454 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2116, 20ja 186 . . . . . . . . . 10 (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
2221com12 32 . . . . . . . . 9 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐵 = 𝐴𝐵 = 𝐵) → 𝑥 = 𝐵) → 𝐴 = 𝐵))
2312, 22syld 47 . . . . . . . 8 ((𝑥 = 𝐴 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
2423ex 413 . . . . . . 7 (𝑥 = 𝐴 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
25 simprll 776 . . . . . . . . . 10 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴𝑉)
26 eqeq1 2742 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐴𝐴 = 𝐴))
27 eqeq1 2742 . . . . . . . . . . . . 13 (𝑦 = 𝐴 → (𝑦 = 𝐵𝐴 = 𝐵))
2826, 27orbi12d 916 . . . . . . . . . . . 12 (𝑦 = 𝐴 → ((𝑦 = 𝐴𝑦 = 𝐵) ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
29 eqeq2 2750 . . . . . . . . . . . 12 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
3028, 29imbi12d 345 . . . . . . . . . . 11 (𝑦 = 𝐴 → (((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) ↔ ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3130rspcv 3557 . . . . . . . . . 10 (𝐴𝑉 → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
3225, 31syl 17 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → ((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴)))
33 ioran 981 . . . . . . . . . . . 12 (¬ (𝐴 = 𝐴𝐴 = 𝐵) ↔ (¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵))
34 eqid 2738 . . . . . . . . . . . . . 14 𝐴 = 𝐴
3534pm2.24i 150 . . . . . . . . . . . . 13 𝐴 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3635adantr 481 . . . . . . . . . . . 12 ((¬ 𝐴 = 𝐴 ∧ ¬ 𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3733, 36sylbi 216 . . . . . . . . . . 11 (¬ (𝐴 = 𝐴𝐴 = 𝐵) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
3817a1d 25 . . . . . . . . . . . 12 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → 𝐴 = 𝐵))
3938expimpd 454 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4037, 39ja 186 . . . . . . . . . 10 (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → 𝐴 = 𝐵))
4140com12 32 . . . . . . . . 9 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (((𝐴 = 𝐴𝐴 = 𝐵) → 𝑥 = 𝐴) → 𝐴 = 𝐵))
4232, 41syld 47 . . . . . . . 8 ((𝑥 = 𝐵 ∧ ((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉)) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵))
4342ex 413 . . . . . . 7 (𝑥 = 𝐵 → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4424, 43jaoi 854 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐵) → (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4544com12 32 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → ((𝑥 = 𝐴𝑥 = 𝐵) → (∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦) → 𝐴 = 𝐵)))
4645impd 411 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝑥𝑉) → (((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
4746rexlimdva 3213 . . 3 ((𝐴𝑉𝐵𝑉) → (∃𝑥𝑉 ((𝑥 = 𝐴𝑥 = 𝐵) ∧ ∀𝑦𝑉 ((𝑦 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝑦)) → 𝐴 = 𝐵))
484, 47syl5bi 241 . 2 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵))
49 reueq 3672 . . . . . . 7 (𝐵𝑉 ↔ ∃!𝑥𝑉 𝑥 = 𝐵)
5049biimpi 215 . . . . . 6 (𝐵𝑉 → ∃!𝑥𝑉 𝑥 = 𝐵)
5150adantl 482 . . . . 5 ((𝐴𝑉𝐵𝑉) → ∃!𝑥𝑉 𝑥 = 𝐵)
5251adantr 481 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 𝑥 = 𝐵)
53 eqeq2 2750 . . . . . . . 8 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
5453adantl 482 . . . . . . 7 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (𝑥 = 𝐴𝑥 = 𝐵))
5554orbi1d 914 . . . . . 6 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ (𝑥 = 𝐵𝑥 = 𝐵)))
56 oridm 902 . . . . . 6 ((𝑥 = 𝐵𝑥 = 𝐵) ↔ 𝑥 = 𝐵)
5755, 56bitrdi 287 . . . . 5 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ((𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝑥 = 𝐵))
5857reubidv 3323 . . . 4 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ ∃!𝑥𝑉 𝑥 = 𝐵))
5952, 58mpbird 256 . . 3 (((𝐴𝑉𝐵𝑉) ∧ 𝐴 = 𝐵) → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵))
6059ex 413 . 2 ((𝐴𝑉𝐵𝑉) → (𝐴 = 𝐵 → ∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵)))
6148, 60impbid 211 1 ((𝐴𝑉𝐵𝑉) → (∃!𝑥𝑉 (𝑥 = 𝐴𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1539  wcel 2106  wral 3064  wrex 3065  ∃!wreu 3066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072
This theorem is referenced by:  quad1  45072  requad1  45074
  Copyright terms: Public domain W3C validator