Theorem brxp 5674

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  ⟨cop 4568   class class class wbr 5079   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631

This theorem is referenced by:  brrelex12  5677  brel  5690  brinxp2  5703  eqbrrdva  5818  ssrelrn  5843  dmxp  5878  xpidtr  6079  xpco  6247  dfpo2  6254  predtrss  6280  isocnv3  7283  tpostpos  8193  brinxper  8670  swoer  8672  erinxp  8735  ecopover  8765  infxpenlem  9933  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  ltxrlt  11214  ltxr  13064  xpcogend  14934  invfuc  17942  elhoma  17997  efglem  19689  gsumcom3fi  19952  gsumdixp  20296  znleval  21536  gsumbagdiag  21914  psrass1lem  21915  opsrtoslem2  22039  lenlts  27741  zsoring  28426  brelg  32706  posrasymb  33053  trleile  33057  ecxpid  33451  qusxpid  33453  metider  34085  satefvfmla1  35660  mclsppslem  35818  xpab  35961  dfon3  36125  brbigcup  36131  brsingle  36150  brimage  36159  brcart  36165  brapply  36171  brcup  36172  brcap  36173  funpartlem  36177  dfrdg4  36186  brub  36189  bj-xpcossxp  37556  itg2gt0cn  38049  grucollcld  44711  grumnud  44737  coxp  49330  xpco2  49354