Theorem brxp 5017

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 4435	. 2 |- ( A ( C X. D ) B <-> <. A , B >. e. ( C X. D ) )
2		opelxp 5016	. 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 1802   <.cop 4017   class class class wbr 4434   X. cxp 4984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435  df-opab 4493  df-xp 4992

This theorem is referenced by:  brrelex12  5024  brel  5035  brinxp2  5048  eqbrrdva  5159  xpidtr  5376  xpco  5534  isocnv3  6210  tpostpos  6974  swoer  7338  erinxp  7384  ecopover  7414  dfsup2OLD  7902  infxpenlem  8391  fpwwe2lem6  9013  fpwwe2lem7  9014  fpwwe2lem9  9016  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  ltxrlt  9655  ltxr  11330  xpsfrnel2  14836  invfuc  15214  elhoma  15230  efglem  16605  gsumdixpOLD  17128  gsumdixp  17129  gsumbagdiag  17899  psrass1lem  17900  opsrtoslem2  18020  znleval  18463  gsumcom3fi  18772  brelg  27331  posrasymb  27515  trleile  27524  metider  27743  mclsppslem  28813  dfpo2  29156  dfon3  29514  brbigcup  29520  brsingle  29539  brimage  29548  brcart  29554  brapply  29560  brcup  29561  brcap  29562  funpartlem  29564  dfrdg4  29572  brub  29576  itg2gt0cn  30042  xpcogend  37449