Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brtp Structured version   Visualization version   GIF version

Theorem brtp 31400
 Description: A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypotheses
Ref Expression
brtp.1 𝑋 ∈ V
brtp.2 𝑌 ∈ V
Assertion
Ref Expression
brtp (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴𝑌 = 𝐵) ∨ (𝑋 = 𝐶𝑌 = 𝐷) ∨ (𝑋 = 𝐸𝑌 = 𝐹)))

Proof of Theorem brtp
StepHypRef Expression
1 df-br 4624 . 2 (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})
2 opex 4903 . . 3 𝑋, 𝑌⟩ ∈ V
32eltp 4208 . 2 (⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} ↔ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩))
4 brtp.1 . . . 4 𝑋 ∈ V
5 brtp.2 . . . 4 𝑌 ∈ V
64, 5opth 4915 . . 3 (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑋 = 𝐴𝑌 = 𝐵))
74, 5opth 4915 . . 3 (⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑋 = 𝐶𝑌 = 𝐷))
84, 5opth 4915 . . 3 (⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑋 = 𝐸𝑌 = 𝐹))
96, 7, 83orbi123i 1250 . 2 ((⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩) ↔ ((𝑋 = 𝐴𝑌 = 𝐵) ∨ (𝑋 = 𝐶𝑌 = 𝐷) ∨ (𝑋 = 𝐸𝑌 = 𝐹)))
101, 3, 93bitri 286 1 (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴𝑌 = 𝐵) ∨ (𝑋 = 𝐶𝑌 = 𝐷) ∨ (𝑋 = 𝐸𝑌 = 𝐹)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   ∨ w3o 1035   = wceq 1480   ∈ wcel 1987  Vcvv 3190  {ctp 4159  ⟨cop 4161   class class class wbr 4623 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-br 4624 This theorem is referenced by:  sltval2  31563  sltsgn1  31568  sltsgn2  31569  sltintdifex  31570  sltres  31571  noextendlt  31579  noextendgt  31580  sltsolem1  31581  nodenselem8  31604  nodense  31605  nobndup  31616  nobnddown  31617  nosepnelem  31618  nosepdmlem  31620
 Copyright terms: Public domain W3C validator