Theorem brxp 5699

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  ⟨cop 4834   class class class wbr 5102   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656

This theorem is used by:  brrelex12  5702  brel  5715  brinxp2  5728  eqbrrdva  5846  ssrelrn  5875  dmxp  5910  xpidtr  6115  cnvxp  6146  xpco  6292  dfpo2  6299  predtrss  6325  isocnv3  7340  tpostpos  8266  brinxper  8750  swoer  8752  erinxp  8815  ecopover  8845  infxpenlem  10095  fpwwe2lem5  10723  fpwwe2lem6  10724  fpwwe2lem8  10726  fpwwe2lem11  10729  fpwwe2lem12  10730  fpwwe2  10731  ltxrlt  11383  ltxr  13247  xpcogend  15132  invfuc  18157  elhoma  18212  ecxpid  19391  qusxpid  19400  efglem  19935  gsumcom3fi  20198  gsumdixp  20553  znleval  21865  gsumbagdiag  22245  psrass1lem  22246  opsrtoslem2  22370  lenlts  28114  zsoring  28800  brelg  33248  posrasymb  33574  trleile  33578  metider  34572  satefvfmla1  36276  mclsppslem  36434  xpab  36583  dfon3  36746  brbigcup  36752  brsingle  36771  brimage  36780  brcart  36786  brapply  36792  brcup  36793  brcap  36794  funpartlem  36798  dfrdg4  36807  brub  36810  bj-xpcossxp  38203  itg2gt0cn  38686  grucollcld  45337  grumnud  45363  coxp  50037  xpco2  50061