Theorem brxp 5715

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  ⟨cop 4600   class class class wbr 5114   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672

This theorem is used by:  brrelex12  5718  brel  5731  brinxp2  5744  eqbrrdva  5860  ssrelrn  5889  dmxp  5924  xpidtr  6127  xpco  6297  dfpo2  6304  predtrss  6330  isocnv3  7341  tpostpos  8251  brinxper  8733  swoer  8735  erinxp  8798  ecopover  8828  infxpenlem  10016  fpwwe2lem5  10638  fpwwe2lem6  10639  fpwwe2lem8  10641  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  ltxrlt  11298  ltxr  13158  xpcogend  15037  invfuc  18059  elhoma  18114  ecxpid  19273  qusxpid  19282  efglem  19817  gsumcom3fi  20080  gsumdixp  20433  znleval  21741  gsumbagdiag  22119  psrass1lem  22120  opsrtoslem2  22244  lenlts  27953  zsoring  28639  brelg  32989  posrasymb  33318  trleile  33322  metider  34315  satefvfmla1  35938  mclsppslem  36096  xpab  36239  dfon3  36403  brbigcup  36409  brsingle  36428  brimage  36437  brcart  36443  brapply  36449  brcup  36450  brcap  36451  funpartlem  36455  dfrdg4  36464  brub  36467  bj-xpcossxp  37874  itg2gt0cn  38367  grucollcld  45011  grumnud  45037  coxp  49652  xpco2  49676