Theorem brxp 5673

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  ⟨cop 4586   class class class wbr 5098   × cxp 5622

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630

This theorem is referenced by:  brrelex12  5676  brel  5689  brinxp2  5702  eqbrrdva  5818  ssrelrn  5843  dmxp  5878  xpidtr  6079  xpco  6247  dfpo2  6254  predtrss  6280  isocnv3  7278  tpostpos  8188  brinxper  8664  swoer  8666  erinxp  8728  ecopover  8758  infxpenlem  9923  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  ltxrlt  11203  ltxr  13029  xpcogend  14897  invfuc  17901  elhoma  17956  efglem  19645  gsumcom3fi  19908  gsumdixp  20254  znleval  21509  gsumbagdiag  21887  psrass1lem  21888  opsrtoslem2  22011  lenlts  27720  zsoring  28405  brelg  32685  posrasymb  33049  trleile  33053  ecxpid  33442  qusxpid  33444  metider  34051  satefvfmla1  35619  mclsppslem  35777  xpab  35920  dfon3  36084  brbigcup  36090  brsingle  36109  brimage  36118  brcart  36124  brapply  36130  brcup  36131  brcap  36132  funpartlem  36136  dfrdg4  36145  brub  36148  bj-xpcossxp  37390  itg2gt0cn  37872  grucollcld  44497  grumnud  44523  coxp  49074  xpco2  49098