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

Theorem brxp 5681
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 5106 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2 opelxp 5669 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
31, 2bitri 274 1 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wcel 2106  cop 4592   class class class wbr 5105   × cxp 5631
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-xp 5639
This theorem is referenced by:  brrelex12  5684  brel  5697  brinxp2  5709  eqbrrdva  5825  ssrelrn  5850  xpidtr  6076  xpco  6241  dfpo2  6248  predtrss  6276  isocnv3  7276  tpostpos  8176  swoer  8677  erinxp  8729  ecopover  8759  infxpenlem  9948  fpwwe2lem5  10570  fpwwe2lem6  10571  fpwwe2lem8  10573  fpwwe2lem11  10576  fpwwe2lem12  10577  fpwwe2  10578  ltxrlt  11224  ltxr  13035  xpcogend  14858  invfuc  17862  elhoma  17917  efglem  19496  gsumcom3fi  19754  gsumdixp  20031  znleval  20959  gsumbagdiagOLD  21339  psrass1lemOLD  21340  gsumbagdiag  21342  psrass1lem  21343  opsrtoslem2  21461  slenlt  27098  brelg  31475  posrasymb  31769  trleile  31775  ecxpid  32092  qusxpid  32095  metider  32415  satefvfmla1  33959  mclsppslem  34117  xpab  34237  dfon3  34467  brbigcup  34473  brsingle  34492  brimage  34501  brcart  34507  brapply  34513  brcup  34514  brcap  34515  funpartlem  34517  dfrdg4  34526  brub  34529  bj-xpcossxp  35650  itg2gt0cn  36123  grucollcld  42521  grumnud  42547
  Copyright terms: Public domain W3C validator