Theorem brxp 5673

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630

This theorem is referenced by:  brrelex12  5676  brel  5689  brinxp2  5702  eqbrrdva  5818  ssrelrn  5843  dmxp  5878  xpidtr  6079  xpco  6247  dfpo2  6254  predtrss  6280  isocnv3  7280  tpostpos  8189  brinxper  8666  swoer  8668  erinxp  8731  ecopover  8761  infxpenlem  9926  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  ltxrlt  11207  ltxr  13057  xpcogend  14927  invfuc  17935  elhoma  17990  efglem  19682  gsumcom3fi  19945  gsumdixp  20289  znleval  21544  gsumbagdiag  21921  psrass1lem  21922  opsrtoslem2  22044  lenlts  27730  zsoring  28415  brelg  32695  posrasymb  33042  trleile  33046  ecxpid  33436  qusxpid  33438  metider  34054  satefvfmla1  35623  mclsppslem  35781  xpab  35924  dfon3  36088  brbigcup  36094  brsingle  36113  brimage  36122  brcart  36128  brapply  36134  brcup  36135  brcap  36136  funpartlem  36140  dfrdg4  36149  brub  36152  bj-xpcossxp  37519  itg2gt0cn  38010  grucollcld  44705  grumnud  44731  coxp  49320  xpco2  49344