Theorem brxp 5734

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ⟨cop 4632   class class class wbr 5143   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691

This theorem is referenced by:  brrelex12  5737  brel  5750  brinxp2  5763  eqbrrdva  5880  ssrelrn  5905  dmxp  5939  xpidtr  6142  xpco  6309  dfpo2  6316  predtrss  6343  isocnv3  7352  tpostpos  8271  brinxper  8774  swoer  8776  erinxp  8831  ecopover  8861  infxpenlem  10053  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  ltxrlt  11331  ltxr  13157  xpcogend  15013  invfuc  18022  elhoma  18077  efglem  19734  gsumcom3fi  19997  gsumdixp  20316  znleval  21573  gsumbagdiag  21951  psrass1lem  21952  opsrtoslem2  22080  slenlt  27797  brelg  32621  posrasymb  32955  trleile  32961  ecxpid  33389  qusxpid  33391  metider  33893  satefvfmla1  35430  mclsppslem  35588  xpab  35726  dfon3  35893  brbigcup  35899  brsingle  35918  brimage  35927  brcart  35933  brapply  35939  brcup  35940  brcap  35941  funpartlem  35943  dfrdg4  35952  brub  35955  bj-xpcossxp  37190  itg2gt0cn  37682  grucollcld  44279  grumnud  44305  coxp  48744