Theorem brxp 5712

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ⟨cop 4596   class class class wbr 5110   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669

This theorem is referenced by:  brrelex12  5715  brel  5728  brinxp2  5741  eqbrrdva  5857  ssrelrn  5886  dmxp  5921  xpidtr  6124  xpco  6292  dfpo2  6299  predtrss  6325  isocnv3  7332  tpostpos  8243  brinxper  8725  swoer  8727  erinxp  8790  ecopover  8820  infxpenlem  9998  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  fpwwe2lem11  10627  fpwwe2lem12  10628  fpwwe2  10629  ltxrlt  11281  ltxr  13141  xpcogend  15013  invfuc  18035  elhoma  18090  ecxpid  19243  qusxpid  19252  efglem  19787  gsumcom3fi  20050  gsumdixp  20401  znleval  21685  gsumbagdiag  22063  psrass1lem  22064  opsrtoslem2  22188  lenlts  27894  zsoring  28580  brelg  32930  posrasymb  33265  trleile  33269  metider  34262  satefvfmla1  35895  mclsppslem  36053  xpab  36196  dfon3  36360  brbigcup  36366  brsingle  36385  brimage  36394  brcart  36400  brapply  36406  brcup  36407  brcap  36408  funpartlem  36412  dfrdg4  36421  brub  36424  bj-xpcossxp  37811  itg2gt0cn  38304  grucollcld  44950  grumnud  44976  coxp  49588  xpco2  49612