Theorem brxp 5680

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5085   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637

This theorem is referenced by:  brrelex12  5683  brel  5696  brinxp2  5709  eqbrrdva  5824  ssrelrn  5849  dmxp  5884  xpidtr  6085  xpco  6253  dfpo2  6260  predtrss  6286  isocnv3  7287  tpostpos  8196  brinxper  8673  swoer  8675  erinxp  8738  ecopover  8768  infxpenlem  9935  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  ltxrlt  11216  ltxr  13066  xpcogend  14936  invfuc  17944  elhoma  17999  efglem  19691  gsumcom3fi  19954  gsumdixp  20298  znleval  21534  gsumbagdiag  21911  psrass1lem  21912  opsrtoslem2  22034  lenlts  27716  zsoring  28401  brelg  32680  posrasymb  33027  trleile  33031  ecxpid  33421  qusxpid  33423  metider  34038  satefvfmla1  35607  mclsppslem  35765  xpab  35908  dfon3  36072  brbigcup  36078  brsingle  36097  brimage  36106  brcart  36112  brapply  36118  brcup  36119  brcap  36120  funpartlem  36124  dfrdg4  36133  brub  36136  bj-xpcossxp  37503  itg2gt0cn  37996  grucollcld  44687  grumnud  44713  coxp  49308  xpco2  49332