Theorem brxp 4857

Description: Binary relation on a Cartesian 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

Step	Hyp	Ref	Expression
1		df-br 4281	. 2 |- ( A ( C X. D ) B <-> <. A , B >. e. ( C X. D ) )
2		opelxp 4856	. 2 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
3	1, 2	bitri 249	1 |- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )

Syntax hints:   <-> wb 184   /\ wa 369   e. wcel 1755   <.cop 3871   class class class wbr 4280   X. cxp 4825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833

This theorem is referenced by:  brrelex12  4863  brel  4874  brinxp2  4887  eqbrrdva  4996  xpidtr  5208  xpco  5365  isocnv3  6010  tpostpos  6754  swoer  7117  erinxp  7162  ecopover  7192  dfsup2OLD  7681  infxpenlem  8168  fpwwe2lem6  8790  fpwwe2lem7  8791  fpwwe2lem9  8793  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwe2  8798  ltxrlt  9433  ltxr  11083  xpsfrnel2  14486  invfuc  14867  elhoma  14883  efglem  16193  gsumdixpOLD  16635  gsumdixp  16636  gsumbagdiag  17380  psrass1lem  17381  opsrtoslem2  17498  znleval  17829  gsumcom3fi  18142  brelg  25765  posrasymb  25941  trleile  25950  metider  26175  dfpo2  27412  dfon3  27770  brbigcup  27776  brsingle  27795  brimage  27804  brcart  27810  brapply  27816  brcup  27817  brcap  27818  funpartlem  27820  dfrdg4  27828  brub  27832  itg2gt0cn  28291