Theorem brxp 5737

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  ⟨cop 4636   class class class wbr 5147   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694

This theorem is referenced by:  brrelex12  5740  brel  5753  brinxp2  5765  eqbrrdva  5882  ssrelrn  5907  dmxp  5941  xpidtr  6144  xpco  6310  dfpo2  6317  predtrss  6344  isocnv3  7351  tpostpos  8269  brinxper  8772  swoer  8774  erinxp  8829  ecopover  8859  infxpenlem  10050  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem8  10675  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  ltxrlt  11328  ltxr  13154  xpcogend  15009  invfuc  18030  elhoma  18085  efglem  19748  gsumcom3fi  20011  gsumdixp  20332  znleval  21590  gsumbagdiag  21968  psrass1lem  21969  opsrtoslem2  22097  slenlt  27811  brelg  32628  posrasymb  32939  trleile  32945  ecxpid  33368  qusxpid  33370  metider  33854  satefvfmla1  35409  mclsppslem  35567  xpab  35705  dfon3  35873  brbigcup  35879  brsingle  35898  brimage  35907  brcart  35913  brapply  35919  brcup  35920  brcap  35921  funpartlem  35923  dfrdg4  35932  brub  35935  bj-xpcossxp  37171  itg2gt0cn  37661  grucollcld  44255  grumnud  44281