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

Theorem brtp 5533
Description: A necessary and sufficient condition for two sets to be related under a binary relation which is 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 5149 . 2 (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})
2 opex 5475 . . 3 𝑋, 𝑌⟩ ∈ V
32eltp 4694 . 2 (⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} ↔ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩))
4 brtp.1 . . . 4 𝑋 ∈ V
5 brtp.2 . . . 4 𝑌 ∈ V
64, 5opth 5487 . . 3 (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑋 = 𝐴𝑌 = 𝐵))
74, 5opth 5487 . . 3 (⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑋 = 𝐶𝑌 = 𝐷))
84, 5opth 5487 . . 3 (⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑋 = 𝐸𝑌 = 𝐹))
96, 7, 83orbi123i 1155 . 2 ((⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩) ↔ ((𝑋 = 𝐴𝑌 = 𝐵) ∨ (𝑋 = 𝐶𝑌 = 𝐷) ∨ (𝑋 = 𝐸𝑌 = 𝐹)))
101, 3, 93bitri 297 1 (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴𝑌 = 𝐵) ∨ (𝑋 = 𝐶𝑌 = 𝐷) ∨ (𝑋 = 𝐸𝑌 = 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3o 1085   = wceq 1537  wcel 2106  Vcvv 3478  {ctp 4635  cop 4637   class class class wbr 5148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-br 5149
This theorem is referenced by:  sltval2  27716  sltintdifex  27721  sltres  27722  noextendlt  27729  noextendgt  27730  nolesgn2o  27731  nogesgn1o  27733  sltsolem1  27735  nosepnelem  27739  nosep1o  27741  nosep2o  27742  nosepdmlem  27743  nodenselem8  27751  nodense  27752  nolt02o  27755  nogt01o  27756  nosupbnd2lem1  27775  noinfbnd2lem1  27790
  Copyright terms: Public domain W3C validator