Theorem brxp 5687

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ⟨cop 4595   class class class wbr 5107   × cxp 5636

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644

This theorem is referenced by:  brrelex12  5690  brel  5703  brinxp2  5716  eqbrrdva  5833  ssrelrn  5858  dmxp  5892  xpidtr  6095  xpco  6262  dfpo2  6269  predtrss  6295  isocnv3  7307  tpostpos  8225  brinxper  8700  swoer  8702  erinxp  8764  ecopover  8794  infxpenlem  9966  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  ltxrlt  11244  ltxr  13075  xpcogend  14940  invfuc  17939  elhoma  17994  efglem  19646  gsumcom3fi  19909  gsumdixp  20228  znleval  21464  gsumbagdiag  21840  psrass1lem  21841  opsrtoslem2  21963  slenlt  27664  brelg  32537  posrasymb  32891  trleile  32897  ecxpid  33332  qusxpid  33334  metider  33884  satefvfmla1  35412  mclsppslem  35570  xpab  35713  dfon3  35880  brbigcup  35886  brsingle  35905  brimage  35914  brcart  35920  brapply  35926  brcup  35927  brcap  35928  funpartlem  35930  dfrdg4  35939  brub  35942  bj-xpcossxp  37177  itg2gt0cn  37669  grucollcld  44249  grumnud  44275  coxp  48821  xpco2  48845