Theorem brxp 5672

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 5096	. 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2		opelxp 5659	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
3	1, 2	bitri 275	1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ⟨cop 4585   class class class wbr 5095   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629

This theorem is referenced by:  brrelex12  5675  brel  5688  brinxp2  5701  eqbrrdva  5816  ssrelrn  5841  dmxp  5875  xpidtr  6075  xpco  6241  dfpo2  6248  predtrss  6274  isocnv3  7273  tpostpos  8186  brinxper  8661  swoer  8663  erinxp  8725  ecopover  8755  infxpenlem  9926  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  ltxrlt  11204  ltxr  13035  xpcogend  14899  invfuc  17902  elhoma  17957  efglem  19613  gsumcom3fi  19876  gsumdixp  20222  znleval  21479  gsumbagdiag  21856  psrass1lem  21857  opsrtoslem2  21979  slenlt  27680  zsoring  28319  brelg  32570  posrasymb  32922  trleile  32926  ecxpid  33308  qusxpid  33310  metider  33860  satefvfmla1  35397  mclsppslem  35555  xpab  35698  dfon3  35865  brbigcup  35871  brsingle  35890  brimage  35899  brcart  35905  brapply  35911  brcup  35912  brcap  35913  funpartlem  35915  dfrdg4  35924  brub  35927  bj-xpcossxp  37162  itg2gt0cn  37654  grucollcld  44233  grumnud  44259  coxp  48818  xpco2  48842