MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdva Structured version   Visualization version   GIF version

Theorem rexlimdva 3012
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexlimdva (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 448 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3011 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  rexlimdvaa  3013  rexlimivv  3017  rexlimdvv  3018  ssexnelpss  3681  ralxfrdOLD  4800  ralxfrd2  4804  otiunsndisj  4895  elsnxp  5579  foco2  6271  foco2OLD  6272  elunirn  6390  f1elima  6398  tfrlem9a  7346  seqomlem2  7410  oawordexr  7500  odi  7523  oelimcl  7544  nnawordex  7581  nnaordex  7582  oaabs  7588  oaabs2  7589  omabs  7591  ectocld  7678  onfin  8013  dif1en  8055  isfinite2  8080  isfiniteg  8082  fofinf1o  8103  elfiun  8196  suplub2  8227  supisoex  8240  ordtypelem9  8291  ordtypelem10  8292  brwdom2  8338  brwdom3  8347  rankr1ai  8521  fodomfi2  8743  infpwfien  8745  dfac12r  8828  ackbij1  8920  cff1  8940  fin23lem21  9021  isf32lem2  9036  fin1a2lem11  9092  fin1a2lem13  9094  ficard  9243  pwcfsdom  9261  gchina  9377  eltsk2g  9429  tskr1om2  9446  rankcf  9455  inatsk  9456  tskuni  9461  nqereu  9607  ltexnq  9653  1idpr  9707  suplem1pr  9730  supsrlem  9788  axpre-sup  9846  1re  9895  negfi  10822  fiminre  10823  supaddc  10839  supadd  10840  supmul1  10841  supmul  10844  suprzcl2  11612  qmulz  11625  qbtwnre  11865  ioo0  12029  ico0  12050  ioc0  12051  icc0  12052  modmuladd  12531  modmuladdnn0  12533  addmodlteq  12564  fsequb  12593  ssnn0fi  12603  hashdom  12983  reuccats1lem  13279  reuccats1  13280  2cshwcshw  13370  wrdl3s3  13501  s3iunsndisj  13503  shftlem  13604  rexuzre  13888  rexico  13889  caubnd  13894  limsupbnd1  14009  limsupbnd2  14010  rlim2lt  14024  rlim3  14025  lo1bdd2  14051  lo1bddrp  14052  o1lo1  14064  climuni  14079  climshftlem  14101  o1co  14113  rlimcn1  14115  climcn1  14118  o1rlimmul  14145  lo1le  14178  rlimno1  14180  isercoll  14194  caurcvg2  14204  serf0  14207  summolem2  14242  zsum  14244  fsum2dlem  14291  geomulcvg  14394  mertenslem2  14404  ntrivcvg  14416  zprod  14454  fprod2dlem  14497  dvds1lem  14779  odd2np1lem  14850  odd2np1  14851  mod2eq1n2dvds  14857  sqoddm1div8z  14864  ltoddhalfle  14871  halfleoddlt  14872  m1expo  14878  flodddiv4  14923  dvdssqim  15059  coprmdvds2  15154  divgcdcoprm0  15165  cncongr1  15167  cncongr2  15168  dvdsnprmd  15189  isprm5  15205  rpexp  15218  ncoprmlnprm  15222  pythagtriplem1  15307  iserodd  15326  pc2dvds  15369  difsqpwdvds  15377  oddprmdvds  15393  prmpwdvds  15394  4sqlem11  15445  vdwapun  15464  vdwlem2  15472  vdwlem6  15476  vdwlem8  15478  vdwlem10  15480  vdwnnlem1  15485  vdwnnlem3  15487  0ram  15510  ramub1lem2  15517  ramcl  15519  cshwsiun  15592  cshwrepswhash1  15595  firest  15864  imasvscafn  15968  imasmnd2  17098  dfgrp3lem  17284  imasgrp2  17301  issubg4  17384  gaorber  17512  orbsta  17517  pmtr3ncom  17666  psgnran  17706  odmulg  17744  odbezout  17746  gexdvdsi  17769  sylow1lem3  17786  odcau  17790  sylow2alem1  17803  sylow3lem6  17818  lsmelvalm  17837  efgrelexlemb  17934  efgredeu  17936  cyggeninv  18056  cygctb  18064  cyggexb  18071  dprdssv  18186  dprddisj2  18209  ablfacrplem  18235  pgpfac1lem2  18245  pgpfac1lem5  18249  ringinvnz1ne0  18363  ringinvnzdiv  18364  imasring  18390  dvdsrcl2  18421  dvdsrmul1  18424  lss1d  18732  lssats2  18769  lspsn  18771  lmhmima  18816  lspsneleq  18884  lpiss  19019  mplcoe5lem  19236  mpfind  19305  cply1coe0bi  19439  gsummoncoe1  19443  mpfpf1  19484  pf1mpf  19485  dvdsrzring  19598  znunit  19678  znrrg  19680  cygznlem3  19684  frgpcyg  19688  psgnghm  19692  psgndif  19714  lindfrn  19926  islinds4  19940  mat1dimelbas  20043  mat1dimcrng  20049  scmatdmat  20087  scmataddcl  20088  scmatsubcl  20089  scmatmulcl  20090  smatvscl  20096  cpmatacl  20287  cpmatinvcl  20288  pmatcollpw3fi1lem2  20358  chpscmat  20413  tgcl  20531  clsval2  20611  neindisj  20678  innei  20686  restcld  20733  restcldr  20735  ordtrest2lem  20764  cnprest  20850  lmss  20859  lmcls  20863  lmcnp  20865  isnrm3  20920  isreg2  20938  cmpcovf  20951  cncmp  20952  cmpsub  20960  1stcrest  21013  2ndcrest  21014  dis2ndc  21020  1stccnp  21022  restnlly  21042  cldllycmp  21055  locfincmp  21086  txcnpi  21168  pthaus  21198  txtube  21200  txcmplem1  21201  txcmplem2  21202  txlm  21208  xkohaus  21213  xkococnlem  21219  xkococn  21220  kqfvima  21290  kqreglem1  21301  isfild  21419  fgcl  21439  filuni  21446  isufil2  21469  ufileu  21480  uffix  21482  rnelfm  21514  fmfnfmlem2  21516  fmfnfmlem4  21518  fmfnfm  21519  fmco  21522  fclsopn  21575  ufilcmp  21593  cnpfcf  21602  alexsublem  21605  alexsubALT  21612  cldsubg  21671  ghmcnp  21675  qustgpopn  21680  tsmsgsum  21699  tsmsres  21704  tsmsxplem1  21713  tsmsxp  21715  isucn2  21840  ucnprima  21843  imasdsf1olem  21935  blssps  21986  blss  21987  blssexps  21988  blssex  21989  mopni3  22056  blcld  22067  metrest  22086  metcnp3  22102  reperflem  22376  icccmplem3  22382  xrge0tsms  22392  mulc1cncf  22463  cncfco  22465  cnheibor  22509  bndth  22512  lebnumlem3  22517  xlebnum  22519  lebnumii  22520  nmhmcn  22675  cfil3i  22819  cmetcaulem  22838  cfilres  22846  bcthlem4  22876  bcthlem5  22877  ivthlem2  22972  ivthlem3  22973  ivthicc  22978  cniccbdd  22981  ovolunlem1  23016  ovoliunlem2  23022  ovolshftlem2  23029  ovolicc2  23041  iundisj  23067  iunmbl2  23076  dyadmax  23116  opnmbllem  23119  subopnmbl  23122  volivth  23125  vitalilem2  23128  ismbf3d  23171  mbfimaopn2  23174  mbfaddlem  23177  i1fmullem  23211  mbfi1fseqlem4  23235  ellimc3  23393  dvlip  23504  dvlip2  23506  c1liplem1  23507  dvgt0lem1  23513  dvivthlem2  23520  dvne0  23522  lhop1lem  23524  lhop2  23526  lhop  23527  tdeglem4  23568  mdegnn0cl  23579  ply1divex  23644  dvdsq1p  23668  ig1peu  23679  elply2  23700  plypf1  23716  plydivex  23800  aalioulem3  23837  aalioulem5  23839  aaliou  23841  ulmshftlem  23891  ulmcau  23897  ulmss  23899  ulmbdd  23900  ulmcn  23901  radcnvlt1  23920  eflogeq  24096  efopn  24148  cxpeq  24242  angpieqvd  24302  dcubic  24317  xrlimcnp  24439  cxploglim  24448  ftalem2  24544  ftalem7  24549  isppw2  24585  dchrptlem1  24733  dchrptlem3  24735  dchrsum2  24737  lgsdchrval  24823  lgsdchr  24824  gausslemma2dlem1a  24834  lgsquadlem1  24849  2lgslem1c  24862  2lgslem3a1  24869  2lgslem3b1  24870  2lgslem3c1  24871  2lgslem3d1  24872  2lgsoddprmlem2  24878  dchrisumlem3  24924  dchrisum0fno1  24944  pntlem3  25042  pntleml  25044  ostth3  25071  brcgr  25525  brbtwn2  25530  axbtwnid  25564  axcontlem7  25595  usgranloop  25701  usgrarnedg1  25711  nbgraf1olem5  25767  wwlkextprop  26065  erclwwlkeqlen  26133  erclwwlktr  26136  clwwlknscsh  26140  erclwwlkneqlen  26145  erclwwlkntr  26148  eleclclwwlkn  26153  hashecclwwlkn1  26154  usghashecclwwlk  26155  el2wlkonot  26189  el2spthonot  26190  el2wlkonotot0  26192  2spontn0vne  26207  vdusgra0nedg  26228  usgravd0nedg  26238  eupai  26287  2pthfrgra  26331  3cyclfrgrarn1  26332  frgraregorufr  26373  frg2wot1  26377  frg2woteq  26380  2spotiundisj  26382  usg2spot2nb  26385  usgreg2spot  26387  2spotmdisj  26388  blocnilem  26836  ubthlem1  26903  ubthlem3  26905  htthlem  26951  shsel3  27351  omlsii  27439  spansncol  27604  nmopun  28050  nmcexi  28062  riesz1  28101  elpjrn  28226  cvcon3  28320  chcv1  28391  atcvatlem  28421  chirredi  28430  br8d  28595  iundisjfi  28735  xrge0tsmsd  28909  ordtrest2NEWlem  29089  lmxrge0  29119  indf1ofs  29208  esumcst  29245  esumfsup  29252  esumpcvgval  29260  measdivcstOLD  29407  eulerpartlemgh  29560  dstfrvunirn  29656  afsval  29795  erdszelem8  30227  erdszelem11  30230  erdsze2lem2  30233  conpcon  30264  sconpi1  30268  cvmsss2  30303  cvmfolem  30308  cvmliftmolem2  30311  cvmliftlem15  30327  cvmlift2lem1  30331  cvmlift3lem4  30351  cvmlift3lem5  30352  mrsub0  30460  mrsubcn  30463  msubrn  30473  msubvrs  30504  dvdspw  30682  br8  30692  br6  30693  br4  30694  trpredtr  30767  frrlem5e  30825  cgrtriv  31072  btwntriv2  31082  btwncomim  31083  btwnswapid  31087  btwnintr  31089  btwnexch3  31090  btwnouttr2  31092  ifscgr  31114  cgrxfr  31125  btwnxfr  31126  btwnconn3  31173  segcon2  31175  brsegle  31178  brsegle2  31179  seglecgr12im  31180  broutsideof3  31196  linethru  31223  elhf2  31245  opnregcld  31288  cldregopn  31289  neibastop2lem  31318  matunitlindflem1  32358  poimirlem16  32378  poimirlem17  32379  poimirlem19  32381  poimirlem20  32382  poimirlem24  32386  poimirlem29  32391  heicant  32397  opnmbllem0  32398  ismblfin  32403  itg2addnclem  32414  itg2addnclem3  32416  itg2gt0cn  32418  bddiblnc  32433  ftc1anclem5  32442  ftc2nc  32447  filbcmb  32488  sdclem1  32492  fdc  32494  incsequz  32497  caushft  32510  istotbnd3  32523  sstotbnd3  32528  equivbnd  32542  cntotbnd  32548  heibor1lem  32561  heibor1  32562  bfplem2  32575  divrngidl  32780  prnc  32819  prtlem10  32951  lshpdisj  33075  cvrcon3b  33365  atnle  33405  hlhgt2  33476  hl0lt1N  33477  hl2at  33492  cvrexchlem  33506  cvratlem  33508  lvolnlelpln  33672  2lplnj  33707  ispsubcl2N  34034  lautcvr  34179  dva1dim  35074  dib1dim  35255  dib1dim2  35258  diclspsn  35284  dih1dimatlem  35419  dihlatat  35427  dihatexv  35428  dihatexv2  35429  lcfrlem9  35640  lcfrlem16  35648  mapdrvallem2  35735  mapd1o  35738  elrfi  36058  isnacs3  36074  eldiophb  36121  diophrw  36123  eldioph2b  36127  diophin  36137  eldiophss  36139  rexrabdioph  36159  diophren  36178  rencldnfilem  36185  pell1234qrdich  36226  pellfundex  36251  jm2.26a  36368  jm2.27  36376  lsmfgcl  36445  kercvrlsm  36454  lmhmfgima  36455  lpirlnr  36489  hbtlem2  36496  hbtlem4  36498  hbtlem6  36501  rngunsnply  36545  restuni3  38116  suplesup  38279  stoweidlem57  38733  stoweidlem61  38737  fourierdlem48  38830  fourierdlem49  38831  sge0le  39083  carageniuncllem2  39195  icoresmbl  39216  hspmbllem2  39300  smflimlem2  39441  smfmullem3  39461  iccpartrn  39752  iccpartiun  39756  iccpartnel  39760  odz2prm2pw  39797  fmtnoprmfac2lem1  39800  fmtnofac2lem  39802  fmtnofac1  39804  prmdvdsfmtnof1lem2  39819  2pwp1prm  39825  mod42tp1mod8  39841  lighneallem2  39845  lighneallem3  39846  lighneallem4  39849  dfodd6  39872  dfeven4  39873  m1expevenALTV  39882  opoeALTV  39916  opeoALTV  39917  gbopos  39965  gbogt5  39968  gboage9  39970  nnsum4primesodd  39996  nnsum4primesoddALTV  39997  nnsum4primeseven  40000  tgblthelfgottOLD  40020  reuccatpfxs1lem  40080  reuccatpfxs1  40081  iunopeqop  40110  otiunsndisjX  40111  umgrnloop  40314  usgrnloopALT  40411  uhgrspansubgrlem  40495  nbuhgr  40546  nbupgr  40547  wwlksnextprop  41099  elwspths2on  41144  2wspiundisj  41147  erclwwlkseqlen  41221  erclwwlkstr  41224  clwwlksnscsh  41228  erclwwlksneqlen  41233  erclwwlksntr  41236  eleclclwwlksn  41241  hashecclwwlksn1  41242  umgrhashecclwwlk  41243  umgr3v3e3cycl  41332  cusconngr  41339  eucrctshift  41392  2pthfrgr  41435  3cyclfrgrrn1  41436  frgrregorufr  41471  frgr2wwlk1  41475  fusgr2wsp2nb  41479  copisnmnd  41580  lidldomn1  41692  uzlidlring  41700  isldepslvec2  42049  m1modmmod  42091  aacllem  42298
  Copyright terms: Public domain W3C validator