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

Theorem brxp 5569
Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004.)
Assertion
Ref Expression
brxp (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))

Proof of Theorem brxp
StepHypRef Expression
1 df-br 5034 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2 opelxp 5559 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
31, 2bitri 278 1 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wcel 2112  cop 4534   class class class wbr 5033   × cxp 5521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529
This theorem is referenced by:  brrelex12  5572  brel  5585  brinxp2  5597  eqbrrdva  5708  ssrelrn  5731  xpidtr  5953  xpco  6112  isocnv3  7068  tpostpos  7899  swoer  8306  erinxp  8358  ecopover  8388  infxpenlem  9428  fpwwe2lem6  10050  fpwwe2lem7  10051  fpwwe2lem9  10053  fpwwe2lem12  10056  fpwwe2lem13  10057  fpwwe2  10058  ltxrlt  10704  ltxr  12502  xpcogend  14329  invfuc  17239  elhoma  17287  efglem  18837  gsumcom3fi  19095  gsumdixp  19358  znleval  20249  gsumbagdiag  20617  psrass1lem  20618  opsrtoslem2  20727  brelg  30376  posrasymb  30673  trleile  30682  ecxpid  30979  qusxpid  30982  metider  31245  satefvfmla1  32780  mclsppslem  32938  dfpo2  33099  slenlt  33339  dfon3  33461  brbigcup  33467  brsingle  33486  brimage  33495  brcart  33501  brapply  33507  brcup  33508  brcap  33509  funpartlem  33511  dfrdg4  33520  brub  33523  bj-xpcossxp  34599  itg2gt0cn  35105  grucollcld  40955  grumnud  40981
  Copyright terms: Public domain W3C validator