Theorem brxp 5694

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  ⟨cop 4587   class class class wbr 5099   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651

This theorem is referenced by:  brrelex12  5697  brel  5710  brinxp2  5723  eqbrrdva  5839  ssrelrn  5868  dmxp  5903  xpidtr  6106  xpco  6272  dfpo2  6279  predtrss  6305  isocnv3  7312  tpostpos  8221  brinxper  8703  swoer  8705  erinxp  8768  ecopover  8798  infxpenlem  9966  fpwwe2lem5  10590  fpwwe2lem6  10591  fpwwe2lem8  10593  fpwwe2lem11  10596  fpwwe2lem12  10597  fpwwe2  10598  ltxrlt  11250  ltxr  13114  xpcogend  14984  invfuc  17993  elhoma  18048  efglem  19739  gsumcom3fi  20002  gsumdixp  20346  znleval  21586  gsumbagdiag  21964  psrass1lem  21965  opsrtoslem2  22089  lenlts  27793  zsoring  28479  brelg  32759  posrasymb  33106  trleile  33110  ecxpid  33508  qusxpid  33510  metider  34152  satefvfmla1  35739  mclsppslem  35897  xpab  36040  dfon3  36204  brbigcup  36210  brsingle  36229  brimage  36238  brcart  36244  brapply  36250  brcup  36251  brcap  36252  funpartlem  36256  dfrdg4  36265  brub  36268  bj-xpcossxp  37645  itg2gt0cn  38138  grucollcld  44800  grumnud  44826  coxp  49418  xpco2  49442