Theorem opelxpi 5709

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 5708	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	biimpri 227	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ⟨cop 4630   × cxp 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-opab 5205  df-xp 5678

This theorem is referenced by:  opelxpii  5710  opelxpd  5711  opelvv  5712  opelvvg  5713  opbrop  5769  elsnxp  6289  reuop  6291  fnbrfvb2  6948  ov3  7578  ovres  7581  fovcdm  7585  fnovrn  7590  ovima0  7594  ovconst2  7595  el2xptp0  8034  opiota  8057  fimaproj  8134  xpord2pred  8144  seqomlem2  8465  brdifun  8747  ecopqsi  8784  brecop  8820  eceqoveq  8832  xpcomco  9078  djulcl  9925  djurcl  9926  djulf1o  9927  djurf1o  9928  djuun  9941  isfin4p1  10330  axdc4lem  10470  canthp1lem2  10668  addpiord  10899  mulpiord  10900  pinq  10942  nqereu  10944  addpipq  10952  addpqnq  10953  mulpipq  10955  mulpqnq  10956  ordpipq  10957  recmulnq  10979  dmrecnq  10983  enreceq  11081  addsrpr  11090  mulsrpr  11091  0r  11095  1sr  11096  m1r  11097  addclsr  11098  mulclsr  11099  axaddf  11160  xrlenlt  11301  uzrdgfni  13947  swrdval  14617  ruclem6  16203  eucalgf  16545  eucalg  16549  qnumdenbi  16707  setscom  17140  strfv2d  17162  setsid  17168  imasaddfnlem  17501  imasaddflem  17503  imasvscafn  17510  imasvscaval  17511  funcpropd  17880  fucco  17945  catcxpccl  18189  catcxpcclOLD  18190  curf1cl  18211  curf2cl  18214  curfcl  18215  uncfcurf  18222  diag2  18228  curf2ndf  18230  joindmss  18362  meetdmss  18376  latlem  18420  latjcom  18430  latmcom  18446  efgmf  19659  efglem  19662  vrgpf  19714  vrgpinv  19715  frgpuplem  19718  frgpup2  19722  frgpnabllem1  19819  gsumxp2  19926  rhmsubclem2  20608  pzriprnglem10  21403  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  matsubgcell  22323  matvscacell  22325  pmatcoe1fsupp  22590  txbas  23458  txcls  23495  upxp  23514  uptx  23516  txtube  23531  txcmplem1  23532  txlm  23539  tx1stc  23541  txkgen  23543  cnmpt21  23562  txswaphmeolem  23695  txswaphmeo  23696  clssubg  24000  qustgplem  24012  comet  24409  txmetcnp  24443  metustsym  24451  nrmmetd  24470  isngp3  24494  ngpds  24500  qtopbaslem  24662  cnmetdval  24674  remetdval  24692  tgqioo  24703  bndth  24871  htpyco2  24892  phtpyco2  24903  ovolicc1  25432  ioorf  25489  ioorcl  25493  itg1addlem4  25615  itg1addlem4OLD  25616  dvcnp2  25836  dvcnp2OLD  25837  dvef  25899  lhop1lem  25933  taylthlem2  26296  taylthlem2OLD  26297  addsqnreup  27363  addsfo  27887  noseqrdgfn  28166  brcgr  28698  ex-fpar  30259  imsdval  30483  sspval  30520  opreu2reuALT  32261  2ndimaxp  32416  ofoprabco  32433  f1od2  32487  qtophaus  33373  mbfmco2  33821  eulerpartlemgh  33934  afsval  34239  erdszelem9  34745  cvmlift2lem1  34848  cvmlift2lem9  34857  cvmlift2lem12  34860  cvmlift2lem13  34861  cvmliftphtlem  34863  goel  34893  goelel3xp  34894  sat1el2xp  34925  fmla0xp  34929  prv1n  34977  msubco  35077  msubff1  35102  mvhf  35104  msubvrs  35106  fvtransport  35564  colinearex  35592  bj-idres  36575  icoreunrn  36774  relowlpssretop  36779  curf  37006  finixpnum  37013  poimirlem15  37043  poimirlem25  37053  poimirlem26  37054  poimirlem27  37055  heicant  37063  mblfinlem1  37065  mblfinlem2  37066  ftc1anc  37109  opropabco  37132  heiborlem5  37223  dvhelvbasei  40498  dvhopvadd  40503  dvhvaddcl  40505  dvhopvsca  40512  dvhvscacl  40513  dvhgrp  40517  dvhopclN  40523  dvhopaddN  40524  dvhopspN  40525  dib1dim2  40578  diblss  40580  diclspsn  40604  dih1dimatlem  40739  hoicvr  45859  hoicvrrex  45867  ovnsubaddlem1  45881  ovnhoilem1  45912  ovnlecvr2  45921  opnvonmbllem1  45943  ovolval4lem2  45961  fnotaovb  46501  aovmpt4g  46504  rngccoALTV  47256  rhmsubcALTVlem2  47267  ringccoALTV  47290  rrx2plordisom  47719