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

Theorem rexlimdva 3013
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 449 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3012 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902
This theorem is referenced by:  rexlimdvaa  3014  rexlimivv  3018  rexlimdvv  3019  ssexnelpss  3682  ralxfrdOLD  4806  ralxfrd2  4810  otiunsndisj  4905  iunopeqop  4906  elsnxp  5594  foco2  6287  foco2OLD  6288  elunirn  6413  f1elima  6421  tfrlem9a  7369  seqomlem2  7433  oawordexr  7523  odi  7546  oelimcl  7567  nnawordex  7604  nnaordex  7605  oaabs  7611  oaabs2  7612  omabs  7614  ectocld  7701  onfin  8036  dif1en  8078  isfinite2  8103  isfiniteg  8105  fofinf1o  8126  elfiun  8219  suplub2  8250  supisoex  8263  ordtypelem9  8314  ordtypelem10  8315  brwdom2  8361  brwdom3  8370  rankr1ai  8544  fodomfi2  8766  infpwfien  8768  dfac12r  8851  ackbij1  8943  cff1  8963  fin23lem21  9044  isf32lem2  9059  fin1a2lem11  9115  fin1a2lem13  9117  ficard  9266  pwcfsdom  9284  gchina  9400  eltsk2g  9452  tskr1om2  9469  rankcf  9478  inatsk  9479  tskuni  9484  nqereu  9630  ltexnq  9676  1idpr  9730  suplem1pr  9753  supsrlem  9811  axpre-sup  9869  1re  9918  negfi  10850  fiminre  10851  supaddc  10867  supadd  10868  supmul1  10869  supmul  10872  suprzcl2  11654  qmulz  11667  qbtwnre  11904  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  modmuladd  12574  modmuladdnn0  12576  addmodlteq  12607  fsequb  12636  ssnn0fi  12646  hashdom  13029  reuccats1lem  13331  reuccats1  13332  2cshwcshw  13422  wrdl3s3  13553  s3iunsndisj  13555  shftlem  13656  rexuzre  13940  rexico  13941  caubnd  13946  limsupbnd1  14061  limsupbnd2  14062  rlim2lt  14076  rlim3  14077  lo1bdd2  14103  lo1bddrp  14104  o1lo1  14116  climuni  14131  climshftlem  14153  o1co  14165  rlimcn1  14167  climcn1  14170  o1rlimmul  14197  lo1le  14230  rlimno1  14232  isercoll  14246  caurcvg2  14256  serf0  14259  summolem2  14294  zsum  14296  fsum2dlem  14343  geomulcvg  14446  mertenslem2  14456  ntrivcvg  14468  zprod  14506  fprod2dlem  14549  dvds1lem  14831  odd2np1lem  14902  odd2np1  14903  mod2eq1n2dvds  14909  sqoddm1div8z  14916  ltoddhalfle  14923  halfleoddlt  14924  m1expo  14930  flodddiv4  14975  dvdssqim  15111  coprmdvds2  15206  divgcdcoprm0  15217  cncongr1  15219  cncongr2  15220  dvdsnprmd  15241  isprm5  15257  rpexp  15270  ncoprmlnprm  15274  pythagtriplem1  15359  iserodd  15378  pc2dvds  15421  difsqpwdvds  15429  oddprmdvds  15445  prmpwdvds  15446  4sqlem11  15497  vdwapun  15516  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  vdwlem10  15532  vdwnnlem1  15537  vdwnnlem3  15539  0ram  15562  ramub1lem2  15569  ramcl  15571  cshwsiun  15644  cshwrepswhash1  15647  firest  15916  imasvscafn  16020  imasmnd2  17150  dfgrp3lem  17336  imasgrp2  17353  issubg4  17436  gaorber  17564  orbsta  17569  pmtr3ncom  17718  psgnran  17758  odmulg  17796  odbezout  17798  gexdvdsi  17821  sylow1lem3  17838  odcau  17842  sylow2alem1  17855  sylow3lem6  17870  lsmelvalm  17889  efgrelexlemb  17986  efgredeu  17988  cyggeninv  18108  cygctb  18116  cyggexb  18123  dprdssv  18238  dprddisj2  18261  ablfacrplem  18287  pgpfac1lem2  18297  pgpfac1lem5  18301  ringinvnz1ne0  18415  ringinvnzdiv  18416  imasring  18442  dvdsrcl2  18473  dvdsrmul1  18476  lss1d  18784  lssats2  18821  lspsn  18823  lmhmima  18868  lspsneleq  18936  lpiss  19071  mplcoe5lem  19288  mpfind  19357  cply1coe0bi  19491  gsummoncoe1  19495  mpfpf1  19536  pf1mpf  19537  dvdsrzring  19650  znunit  19731  znrrg  19733  cygznlem3  19737  frgpcyg  19741  psgnghm  19745  psgndif  19767  lindfrn  19979  islinds4  19993  mat1dimelbas  20096  mat1dimcrng  20102  scmatdmat  20140  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  smatvscl  20149  cpmatacl  20340  cpmatinvcl  20341  pmatcollpw3fi1lem2  20411  chpscmat  20466  tgcl  20584  clsval2  20664  neindisj  20731  innei  20739  restcld  20786  restcldr  20788  ordtrest2lem  20817  cnprest  20903  lmss  20912  lmcls  20916  lmcnp  20918  isnrm3  20973  isreg2  20991  cmpcovf  21004  cncmp  21005  cmpsub  21013  1stcrest  21066  2ndcrest  21067  dis2ndc  21073  1stccnp  21075  restnlly  21095  cldllycmp  21108  locfincmp  21139  txcnpi  21221  pthaus  21251  txtube  21253  txcmplem1  21254  txcmplem2  21255  txlm  21261  xkohaus  21266  xkococnlem  21272  xkococn  21273  kqfvima  21343  kqreglem1  21354  isfild  21472  fgcl  21492  filuni  21499  isufil2  21522  ufileu  21533  uffix  21535  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  fmco  21575  fclsopn  21628  ufilcmp  21646  cnpfcf  21655  alexsublem  21658  alexsubALT  21665  cldsubg  21724  ghmcnp  21728  qustgpopn  21733  tsmsgsum  21752  tsmsres  21757  tsmsxplem1  21766  tsmsxp  21768  isucn2  21893  ucnprima  21896  imasdsf1olem  21988  blssps  22039  blss  22040  blssexps  22041  blssex  22042  mopni3  22109  blcld  22120  metrest  22139  metcnp3  22155  reperflem  22429  icccmplem3  22435  xrge0tsms  22445  mulc1cncf  22516  cncfco  22518  cnheibor  22562  bndth  22565  lebnumlem3  22570  xlebnum  22572  lebnumii  22573  nmhmcn  22728  cfil3i  22875  cmetcaulem  22894  cfilres  22902  bcthlem4  22932  bcthlem5  22933  ivthlem2  23028  ivthlem3  23029  ivthicc  23034  cniccbdd  23037  ovolunlem1  23072  ovoliunlem2  23078  ovolshftlem2  23085  ovolicc2  23097  iundisj  23123  iunmbl2  23132  dyadmax  23172  opnmbllem  23175  subopnmbl  23178  volivth  23181  vitalilem2  23184  ismbf3d  23227  mbfimaopn2  23230  mbfaddlem  23233  i1fmullem  23267  mbfi1fseqlem4  23291  ellimc3  23449  dvlip  23560  dvlip2  23562  c1liplem1  23563  dvgt0lem1  23569  dvivthlem2  23576  dvne0  23578  lhop1lem  23580  lhop2  23582  lhop  23583  tdeglem4  23624  mdegnn0cl  23635  ply1divex  23700  dvdsq1p  23724  ig1peu  23735  elply2  23756  plypf1  23772  plydivex  23856  aalioulem3  23893  aalioulem5  23895  aaliou  23897  ulmshftlem  23947  ulmcau  23953  ulmss  23955  ulmbdd  23956  ulmcn  23957  radcnvlt1  23976  eflogeq  24152  efopn  24204  cxpeq  24298  angpieqvd  24358  dcubic  24373  xrlimcnp  24495  cxploglim  24504  ftalem2  24600  ftalem7  24605  isppw2  24641  dchrptlem1  24789  dchrptlem3  24791  dchrsum2  24793  lgsdchrval  24879  lgsdchr  24880  gausslemma2dlem1a  24890  lgsquadlem1  24905  2lgslem1c  24918  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  2lgsoddprmlem2  24934  dchrisumlem3  24980  dchrisum0fno1  25000  pntlem3  25098  pntleml  25100  ostth3  25127  brcgr  25580  brbtwn2  25585  axbtwnid  25619  axcontlem7  25650  umgrnloop  25774  usgranloop  25908  usgrarnedg1  25918  nbgraf1olem5  25974  wwlkextprop  26272  erclwwlkeqlen  26340  erclwwlktr  26343  clwwlknscsh  26347  erclwwlkneqlen  26352  erclwwlkntr  26355  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  2spontn0vne  26414  vdusgra0nedg  26435  usgravd0nedg  26445  eupai  26494  2pthfrgra  26538  3cyclfrgrarn1  26539  frgraregorufr  26580  frg2wot1  26584  frg2woteq  26587  2spotiundisj  26589  usg2spot2nb  26592  usgreg2spot  26594  2spotmdisj  26595  blocnilem  27043  ubthlem1  27110  ubthlem3  27112  htthlem  27158  shsel3  27558  omlsii  27646  spansncol  27811  nmopun  28257  nmcexi  28269  riesz1  28308  elpjrn  28433  cvcon3  28527  chcv1  28598  atcvatlem  28628  chirredi  28637  br8d  28802  iundisjfi  28942  xrge0tsmsd  29116  ordtrest2NEWlem  29296  lmxrge0  29326  indf1ofs  29415  esumcst  29452  esumfsup  29459  esumpcvgval  29467  measdivcstOLD  29614  eulerpartlemgh  29767  dstfrvunirn  29863  afsval  30002  erdszelem8  30434  erdszelem11  30437  erdsze2lem2  30440  conpcon  30471  sconpi1  30475  cvmsss2  30510  cvmfolem  30515  cvmliftmolem2  30518  cvmliftlem15  30534  cvmlift2lem1  30538  cvmlift3lem4  30558  cvmlift3lem5  30559  mrsub0  30667  mrsubcn  30670  msubrn  30680  msubvrs  30711  dvdspw  30889  br8  30899  br6  30900  br4  30901  trpredtr  30974  frrlem5e  31032  cgrtriv  31279  btwntriv2  31289  btwncomim  31290  btwnswapid  31294  btwnintr  31296  btwnexch3  31297  btwnouttr2  31299  ifscgr  31321  cgrxfr  31332  btwnxfr  31333  btwnconn3  31380  segcon2  31382  brsegle  31385  brsegle2  31386  seglecgr12im  31387  broutsideof3  31403  linethru  31430  elhf2  31452  opnregcld  31495  cldregopn  31496  neibastop2lem  31525  matunitlindflem1  32575  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  poimirlem29  32608  heicant  32614  opnmbllem0  32615  ismblfin  32620  itg2addnclem  32631  itg2addnclem3  32633  itg2gt0cn  32635  bddiblnc  32650  ftc1anclem5  32659  ftc2nc  32664  filbcmb  32705  sdclem1  32709  fdc  32711  incsequz  32714  caushft  32727  istotbnd3  32740  sstotbnd3  32745  equivbnd  32759  cntotbnd  32765  heibor1lem  32778  heibor1  32779  bfplem2  32792  divrngidl  32997  prnc  33036  prtlem10  33168  lshpdisj  33292  cvrcon3b  33582  atnle  33622  hlhgt2  33693  hl0lt1N  33694  hl2at  33709  cvrexchlem  33723  cvratlem  33725  lvolnlelpln  33889  2lplnj  33924  ispsubcl2N  34251  lautcvr  34396  dva1dim  35291  dib1dim  35472  dib1dim2  35475  diclspsn  35501  dih1dimatlem  35636  dihlatat  35644  dihatexv  35645  dihatexv2  35646  lcfrlem9  35857  lcfrlem16  35865  mapdrvallem2  35952  mapd1o  35955  elrfi  36275  isnacs3  36291  eldiophb  36338  diophrw  36340  eldioph2b  36344  diophin  36354  eldiophss  36356  rexrabdioph  36376  diophren  36395  rencldnfilem  36402  pell1234qrdich  36443  pellfundex  36468  jm2.26a  36585  jm2.27  36593  lsmfgcl  36662  kercvrlsm  36671  lmhmfgima  36672  lpirlnr  36706  hbtlem2  36713  hbtlem4  36715  hbtlem6  36718  rngunsnply  36762  restuni3  38333  suplesup  38496  stoweidlem57  38950  stoweidlem61  38954  fourierdlem48  39047  fourierdlem49  39048  sge0le  39300  carageniuncllem2  39412  icoresmbl  39433  hspmbllem2  39517  smflimlem2  39658  smfmullem3  39678  iccpartrn  39968  iccpartiun  39972  iccpartnel  39976  odz2prm2pw  40013  fmtnoprmfac2lem1  40016  fmtnofac2lem  40018  fmtnofac1  40020  prmdvdsfmtnof1lem2  40035  2pwp1prm  40041  mod42tp1mod8  40057  lighneallem2  40061  lighneallem3  40062  lighneallem4  40065  dfodd6  40088  dfeven4  40089  m1expevenALTV  40098  opoeALTV  40132  opeoALTV  40133  gbopos  40181  gbogt5  40184  gboage9  40186  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  tgblthelfgottOLD  40236  reuccatpfxs1lem  40296  reuccatpfxs1  40297  otiunsndisjX  40317  usgrnloopALT  40430  uhgrspansubgrlem  40514  nbuhgr  40565  nbupgr  40566  wwlksnextprop  41118  elwspths2on  41163  2wspiundisj  41166  erclwwlkseqlen  41240  erclwwlkstr  41243  clwwlksnscsh  41247  erclwwlksneqlen  41252  erclwwlksntr  41255  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  umgr3v3e3cycl  41351  cusconngr  41358  eucrctshift  41411  2pthfrgr  41454  3cyclfrgrrn1  41455  frgrregorufr  41490  frgr2wwlk1  41494  fusgr2wsp2nb  41498  copisnmnd  41599  lidldomn1  41711  uzlidlring  41719  isldepslvec2  42068  m1modmmod  42110  aacllem  42356
  Copyright terms: Public domain W3C validator