Theorem brxp 5686

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ⟨cop 4597   class class class wbr 5110   × cxp 5636

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644

This theorem is referenced by:  brrelex12  5689  brel  5702  brinxp2  5714  eqbrrdva  5830  ssrelrn  5855  xpidtr  6081  xpco  6246  dfpo2  6253  predtrss  6281  isocnv3  7282  tpostpos  8182  swoer  8685  erinxp  8737  ecopover  8767  infxpenlem  9958  fpwwe2lem5  10580  fpwwe2lem6  10581  fpwwe2lem8  10583  fpwwe2lem11  10586  fpwwe2lem12  10587  fpwwe2  10588  ltxrlt  11234  ltxr  13045  xpcogend  14871  invfuc  17877  elhoma  17932  efglem  19512  gsumcom3fi  19770  gsumdixp  20047  znleval  20998  gsumbagdiagOLD  21378  psrass1lemOLD  21379  gsumbagdiag  21381  psrass1lem  21382  opsrtoslem2  21500  slenlt  27137  brelg  31595  posrasymb  31895  trleile  31901  ecxpid  32220  qusxpid  32223  metider  32564  satefvfmla1  34106  mclsppslem  34264  xpab  34384  dfon3  34553  brbigcup  34559  brsingle  34578  brimage  34587  brcart  34593  brapply  34599  brcup  34600  brcap  34601  funpartlem  34603  dfrdg4  34612  brub  34615  bj-xpcossxp  35733  itg2gt0cn  36206  grucollcld  42643  grumnud  42669