Theorem brxp 5703

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ⟨cop 4607   class class class wbr 5119   × cxp 5652

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660

This theorem is referenced by:  brrelex12  5706  brel  5719  brinxp2  5732  eqbrrdva  5849  ssrelrn  5874  dmxp  5908  xpidtr  6111  xpco  6278  dfpo2  6285  predtrss  6311  isocnv3  7325  tpostpos  8245  brinxper  8748  swoer  8750  erinxp  8805  ecopover  8835  infxpenlem  10027  fpwwe2lem5  10649  fpwwe2lem6  10650  fpwwe2lem8  10652  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  ltxrlt  11305  ltxr  13131  xpcogend  14993  invfuc  17990  elhoma  18045  efglem  19697  gsumcom3fi  19960  gsumdixp  20279  znleval  21515  gsumbagdiag  21891  psrass1lem  21892  opsrtoslem2  22014  slenlt  27716  brelg  32589  posrasymb  32945  trleile  32951  ecxpid  33376  qusxpid  33378  metider  33925  satefvfmla1  35447  mclsppslem  35605  xpab  35743  dfon3  35910  brbigcup  35916  brsingle  35935  brimage  35944  brcart  35950  brapply  35956  brcup  35957  brcap  35958  funpartlem  35960  dfrdg4  35969  brub  35972  bj-xpcossxp  37207  itg2gt0cn  37699  grucollcld  44284  grumnud  44310  coxp  48811