Theorem brxp 5670

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  ⟨cop 4583   class class class wbr 5095   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  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 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627

This theorem is referenced by:  brrelex12  5673  brel  5686  brinxp2  5699  eqbrrdva  5816  ssrelrn  5841  dmxp  5876  xpidtr  6076  xpco  6244  dfpo2  6251  predtrss  6277  isocnv3  7275  tpostpos  8185  brinxper  8660  swoer  8662  erinxp  8724  ecopover  8754  infxpenlem  9914  fpwwe2lem5  10536  fpwwe2lem6  10537  fpwwe2lem8  10539  fpwwe2lem11  10542  fpwwe2lem12  10543  fpwwe2  10544  ltxrlt  11193  ltxr  13024  xpcogend  14891  invfuc  17894  elhoma  17949  efglem  19638  gsumcom3fi  19901  gsumdixp  20247  znleval  21501  gsumbagdiag  21878  psrass1lem  21879  opsrtoslem2  22001  slenlt  27701  zsoring  28342  brelg  32601  posrasymb  32959  trleile  32963  ecxpid  33337  qusxpid  33339  metider  33918  satefvfmla1  35480  mclsppslem  35638  xpab  35781  dfon3  35945  brbigcup  35951  brsingle  35970  brimage  35979  brcart  35985  brapply  35991  brcup  35992  brcap  35993  funpartlem  35997  dfrdg4  36006  brub  36009  bj-xpcossxp  37244  itg2gt0cn  37725  grucollcld  44367  grumnud  44393  coxp  48947  xpco2  48971