Theorem brxp 5035

Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004.)

Assertion

Ref	Expression
brxp

Proof of Theorem brxp

Step	Hyp	Ref	Expression
1		df-br 4453	. 2
2		opelxp 5034	. 2
3	1, 2	bitri 249	1

Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818  <.cop 4035   class class class wbr 4452  X.cxp 5002

This theorem is referenced by:  brrelex12  5042  brel  5053  brinxp2  5066  eqbrrdva  5177  xpidtr  5394  xpco  5552  isocnv3  6228  tpostpos  6994  swoer  7358  erinxp  7404  ecopover  7434  dfsup2OLD  7923  infxpenlem  8412  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  ltxrlt  9676  ltxr  11353  xpsfrnel2  14962  invfuc  15343  elhoma  15359  efglem  16734  gsumdixpOLD  17257  gsumdixp  17258  gsumbagdiag  18028  psrass1lem  18029  opsrtoslem2  18149  znleval  18593  gsumcom3fi  18902  brelg  27462  posrasymb  27645  trleile  27654  metider  27873  mclsppslem  28943  dfpo2  29184  dfon3  29542  brbigcup  29548  brsingle  29567  brimage  29576  brcart  29582  brapply  29588  brcup  29589  brcap  29590  funpartlem  29592  dfrdg4  29600  brub  29604  itg2gt0cn  30070  xpcogend  37773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010