Theorem brxp 5690

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ⟨cop 4598   class class class wbr 5110   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647

This theorem is referenced by:  brrelex12  5693  brel  5706  brinxp2  5719  eqbrrdva  5836  ssrelrn  5861  dmxp  5895  xpidtr  6098  xpco  6265  dfpo2  6272  predtrss  6298  isocnv3  7310  tpostpos  8228  brinxper  8703  swoer  8705  erinxp  8767  ecopover  8797  infxpenlem  9973  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  ltxrlt  11251  ltxr  13082  xpcogend  14947  invfuc  17946  elhoma  18001  efglem  19653  gsumcom3fi  19916  gsumdixp  20235  znleval  21471  gsumbagdiag  21847  psrass1lem  21848  opsrtoslem2  21970  slenlt  27671  brelg  32544  posrasymb  32898  trleile  32904  ecxpid  33339  qusxpid  33341  metider  33891  satefvfmla1  35419  mclsppslem  35577  xpab  35720  dfon3  35887  brbigcup  35893  brsingle  35912  brimage  35921  brcart  35927  brapply  35933  brcup  35934  brcap  35935  funpartlem  35937  dfrdg4  35946  brub  35949  bj-xpcossxp  37184  itg2gt0cn  37676  grucollcld  44256  grumnud  44282  coxp  48825  xpco2  48849