Theorem brxp 5601

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5066   × cxp 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561

This theorem is referenced by:  brrelex12  5604  brel  5617  brinxp2  5629  eqbrrdva  5740  ssrelrn  5763  xpidtr  5982  xpco  6140  isocnv3  7085  tpostpos  7912  swoer  8319  erinxp  8371  ecopover  8401  infxpenlem  9439  fpwwe2lem6  10057  fpwwe2lem7  10058  fpwwe2lem9  10060  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  ltxrlt  10711  ltxr  12511  xpcogend  14334  invfuc  17244  elhoma  17292  efglem  18842  gsumcom3fi  19099  gsumdixp  19359  gsumbagdiag  20156  psrass1lem  20157  opsrtoslem2  20265  znleval  20701  brelg  30360  posrasymb  30644  trleile  30653  ecxpid  30925  qusxpid  30928  metider  31134  satefvfmla1  32672  mclsppslem  32830  dfpo2  32991  slenlt  33231  dfon3  33353  brbigcup  33359  brsingle  33378  brimage  33387  brcart  33393  brapply  33399  brcup  33400  brcap  33401  funpartlem  33403  dfrdg4  33412  brub  33415  itg2gt0cn  34962  grucollcld  40616  grumnud  40642