MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pr1eqbg Structured version   Visualization version   GIF version

Theorem pr1eqbg 4858
Description: A (proper) pair is equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
Assertion
Ref Expression
pr1eqbg (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))

Proof of Theorem pr1eqbg
StepHypRef Expression
1 eqid 2733 . . . . 5 𝐵 = 𝐵
21biantru 531 . . . 4 (𝐴 = 𝐶 ↔ (𝐴 = 𝐶𝐵 = 𝐵))
32orbi2i 912 . . 3 (((𝐴 = 𝐵𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐵)))
43a1i 11 . 2 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → (((𝐴 = 𝐵𝐵 = 𝐶) ∨ 𝐴 = 𝐶) ↔ ((𝐴 = 𝐵𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐵))))
5 neneq 2947 . . . . 5 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
65adantl 483 . . . 4 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → ¬ 𝐴 = 𝐵)
76intnanrd 491 . . 3 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → ¬ (𝐴 = 𝐵𝐵 = 𝐶))
8 biorf 936 . . 3 (¬ (𝐴 = 𝐵𝐵 = 𝐶) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
97, 8syl 17 . 2 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → (𝐴 = 𝐶 ↔ ((𝐴 = 𝐵𝐵 = 𝐶) ∨ 𝐴 = 𝐶)))
10 3simpa 1149 . . . . 5 ((𝐴𝑈𝐵𝑉𝐶𝑋) → (𝐴𝑈𝐵𝑉))
11 3simpc 1151 . . . . 5 ((𝐴𝑈𝐵𝑉𝐶𝑋) → (𝐵𝑉𝐶𝑋))
1210, 11jca 513 . . . 4 ((𝐴𝑈𝐵𝑉𝐶𝑋) → ((𝐴𝑈𝐵𝑉) ∧ (𝐵𝑉𝐶𝑋)))
1312adantr 482 . . 3 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → ((𝐴𝑈𝐵𝑉) ∧ (𝐵𝑉𝐶𝑋)))
14 preq12bg 4855 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐵𝑉𝐶𝑋)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐵))))
1513, 14syl 17 . 2 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐵))))
164, 9, 153bitr4d 311 1 (((𝐴𝑈𝐵𝑉𝐶𝑋) ∧ 𝐴𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wne 2941  {cpr 4631
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632
This theorem is referenced by:  pr1nebg  4859
  Copyright terms: Public domain W3C validator