Theorem opelxpi 5686

Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opelxpi	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 5685	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 230	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ⟨cop 4590   × cxp 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5165  df-xp 5655

This theorem is referenced by:  opelxpii  5687  opelxpd  5688  opelvv  5689  opelvvg  5690  opbrop  5747  elsnxp  6280  reuop  6282  fnbrfvb2  6924  ov3  7561  ovres  7564  fovcdm  7568  fnovrn  7573  ovima0  7577  ovconst2  7578  el2xptp0  8019  opiota  8042  fimaproj  8117  xpord2pred  8127  seqomlem2  8424  brdifun  8711  ecopqsi  8754  brecop  8794  eceqoveq  8806  xpcomco  9041  djulcl  9870  djurcl  9871  djulf1o  9872  djurf1o  9873  djuun  9886  isfin4p1  10274  axdc4lem  10414  canthp1lem2  10613  addpiord  10844  mulpiord  10845  pinq  10887  nqereu  10889  addpipq  10897  addpqnq  10898  mulpipq  10900  mulpqnq  10901  ordpipq  10902  recmulnq  10924  dmrecnq  10928  enreceq  11026  addsrpr  11035  mulsrpr  11036  0r  11040  1sr  11041  m1r  11042  addclsr  11043  mulclsr  11044  axaddf  11105  xrlenlt  11249  uzrdgfni  13973  swrdval  14659  ruclem6  16269  eucalgf  16619  eucalg  16623  qnumdenbi  16781  setscom  17218  strfv2d  17239  setsid  17245  imasaddfnlem  17560  imasaddflem  17562  imasvscafn  17569  imasvscaval  17570  funcpropd  17937  fucco  18000  catcxpccl  18241  curf1cl  18262  curf2cl  18265  curfcl  18266  uncfcurf  18273  diag2  18279  curf2ndf  18281  joindmss  18411  meetdmss  18425  latlem  18471  latjcom  18481  latmcom  18497  efgmf  19755  efglem  19758  vrgpf  19810  vrgpinv  19811  frgpuplem  19814  frgpup2  19818  frgpnabllem1  19915  gsumxp2  20022  rhmsubclem2  20738  pzriprnglem10  21544  mamudi  22465  mamudir  22466  mamuvs1  22467  mamuvs2  22468  matsubgcell  22496  matvscacell  22498  pmatcoe1fsupp  22763  txbas  23629  txcls  23666  upxp  23685  uptx  23687  txtube  23702  txcmplem1  23703  txlm  23710  tx1stc  23712  txkgen  23714  cnmpt21  23733  txswaphmeolem  23866  txswaphmeo  23867  clssubg  24171  qustgplem  24183  comet  24575  txmetcnp  24609  metustsym  24617  nrmmetd  24636  isngp3  24660  ngpds  24666  qtopbaslem  24820  cnmetdval  24832  remetdval  24851  tgqioo  24862  bndth  25022  htpyco2  25043  phtpyco2  25054  ovolicc1  25580  ioorf  25637  ioorcl  25641  itg1addlem4  25763  dvcnp2  25984  dvef  26044  lhop1lem  26077  taylthlem2  26439  addsqnreup  27509  addsfo  28078  subsfo  28160  noseqrdgfn  28401  brcgr  29103  ex-fpar  30666  imsdval  30891  sspval  30928  opreu2reuALT  32678  2ndimaxp  32850  ofoprabco  32868  f1od2  32923  qtophaus  34135  mbfmco2  34564  eulerpartlemgh  34677  afsval  34970  erdszelem9  35554  cvmlift2lem1  35657  cvmlift2lem9  35666  cvmlift2lem12  35669  cvmlift2lem13  35670  cvmliftphtlem  35672  goel  35702  goelel3xp  35703  sat1el2xp  35734  fmla0xp  35738  prv1n  35786  msubco  35886  msubff1  35911  mvhf  35913  msubvrs  35915  fvtransport  36387  colinearex  36415  nmulprop  36545  bj-idres  37657  icoreunrn  37858  relowlpssretop  37863  curf  38102  finixpnum  38109  poimirlem15  38139  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  heicant  38159  mblfinlem1  38161  mblfinlem2  38162  ftc1anc  38205  opropabco  38228  heiborlem5  38319  dvhelvbasei  41717  dvhopvadd  41722  dvhvaddcl  41724  dvhopvsca  41731  dvhvscacl  41732  dvhgrp  41736  dvhopclN  41742  dvhopaddN  41743  dvhopspN  41744  dib1dim2  41797  diblss  41799  diclspsn  41823  dih1dimatlem  41958  hoicvrrex  47135  ovnsubaddlem1  47149  ovnhoilem1  47180  ovnlecvr2  47189  opnvonmbllem1  47211  ovolval4lem2  47229  fnotaovb  47797  aovmpt4g  47800  rngccoALTV  48898  rhmsubcALTVlem2  48909  ringccoALTV  48932  rrx2plordisom  49350