Theorem brxp 5029

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 4448	. 2 |- ( A ( C X. D ) B <-> <. A , B >. e. ( C X. D ) )
2		opelxp 5028	. 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 1767   <.cop 4033   class class class wbr 4447   X. cxp 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005

This theorem is referenced by:  brrelex12  5036  brel  5047  brinxp2  5060  eqbrrdva  5170  xpidtr  5387  xpco  5545  isocnv3  6214  tpostpos  6972  swoer  7336  erinxp  7382  ecopover  7412  dfsup2OLD  7899  infxpenlem  8387  fpwwe2lem6  9009  fpwwe2lem7  9010  fpwwe2lem9  9012  fpwwe2lem12  9015  fpwwe2lem13  9016  fpwwe2  9017  ltxrlt  9651  ltxr  11320  xpsfrnel2  14816  invfuc  15197  elhoma  15213  efglem  16530  gsumdixpOLD  17041  gsumdixp  17042  gsumbagdiag  17799  psrass1lem  17800  opsrtoslem2  17920  znleval  18360  gsumcom3fi  18669  brelg  27135  posrasymb  27307  trleile  27316  metider  27509  dfpo2  28761  dfon3  29119  brbigcup  29125  brsingle  29144  brimage  29153  brcart  29159  brapply  29165  brcup  29166  brcap  29167  funpartlem  29169  dfrdg4  29177  brub  29181  itg2gt0cn  29647  xpcogend  36783