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

Theorem brxp 4849
Description: Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
Assertion
Ref Expression
brxp  |-  ( A ( C  X.  D
) B  <->  ( A  e.  C  /\  B  e.  D ) )

Proof of Theorem brxp
StepHypRef Expression
1 df-br 4154 . 2  |-  ( A ( C  X.  D
) B  <->  <. A ,  B >.  e.  ( C  X.  D ) )
2 opelxp 4848 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
31, 2bitri 241 1  |-  ( A ( C  X.  D
) B  <->  ( A  e.  C  /\  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    e. wcel 1717   <.cop 3760   class class class wbr 4153    X. cxp 4816
This theorem is referenced by:  brrelex12  4855  brel  4866  brinxp2  4879  eqbrrdva  4982  xpidtr  5196  xpco  5354  isocnv3  5991  tpostpos  6435  swoer  6869  erinxp  6914  ecopover  6944  dfsup2OLD  7383  infxpenlem  7828  fpwwe2lem6  8443  fpwwe2lem7  8444  fpwwe2lem9  8446  fpwwe2lem12  8449  fpwwe2lem13  8450  fpwwe2  8451  ltxrlt  9079  ltxr  10647  xpsfrnel2  13717  invfuc  14098  elhoma  14114  efglem  15275  gsumdixp  15642  gsumbagdiag  16368  psrass1lem  16369  opsrtoslem2  16472  znleval  16758  dfpo2  25136  dfon3  25456  brbigcup  25462  brsingle  25480  brimage  25489  brcart  25495  brapply  25501  brcup  25502  brcap  25503  funpartlem  25505  dfrdg4  25513  itg2gt0cn  25960  gsumcom3fi  27124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824
  Copyright terms: Public domain W3C validator