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

Theorem rexlimdva 3246
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 416 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3245 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  wrex 3110
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 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115
This theorem is referenced by:  rexlimdvaa  3247  rexlimivv  3254  rexlimdvv  3255  ssexnelpss  4044  ralxfrd2  5281  iunopeqop  5379  elsnxp  6114  foco2  6854  elunirn  6992  f1elima  7003  releldmdifi  7730  mpoexw  7763  tfrlem9a  8009  seqomlem2  8074  oawordexr  8169  odi  8192  oelimcl  8213  nnawordex  8250  nnaordex  8251  oaabs  8258  oaabs2  8259  omabs  8261  ectocld  8351  onfin  8698  dif1en  8739  isfinite2  8764  isfiniteg  8766  fofinf1o  8787  elfiun  8882  suplub2  8913  supisoex  8926  ordtypelem9  8978  ordtypelem10  8979  brwdom2  9025  brwdom3  9034  rankr1ai  9215  fodomfi2  9475  infpwfien  9477  dfac12r  9561  ackbij1  9653  cff1  9673  fin23lem21  9754  isf32lem2  9769  fin1a2lem11  9825  fin1a2lem13  9827  ficard  9980  gchina  10114  eltsk2g  10166  tskr1om2  10183  rankcf  10192  inatsk  10193  tskuni  10198  nqereu  10344  ltexnq  10390  1idpr  10444  suplem1pr  10467  supsrlem  10526  axpre-sup  10584  1re  10634  0re  10636  0cnALT  10867  negfi  11581  supaddc  11599  supadd  11600  supmul1  11601  supmul  11604  suprzcl2  12330  qmulz  12343  elpq  12366  qbtwnre  12584  ioo0  12755  ico0  12776  ioc0  12777  icc0  12778  addmodlteq  13313  fsequb  13342  hashdom  13740  ccats1alpha  13968  reuccatpfxs1lem  14103  shftlem  14423  rexuzre  14708  rexico  14709  caubnd  14714  limsupbnd1  14835  limsupbnd2  14836  rlim2lt  14850  rlim3  14851  lo1bdd2  14877  lo1bddrp  14878  o1lo1  14890  climuni  14905  climshftlem  14927  o1co  14939  rlimcn1  14941  climcn1  14944  o1rlimmul  14971  lo1le  15004  rlimno1  15006  isercoll  15020  caurcvg2  15030  serf0  15033  summolem2  15069  zsum  15071  fsum2dlem  15121  geomulcvg  15228  mertenslem2  15237  ntrivcvg  15249  zprod  15287  fprod2dlem  15330  dvds1lem  15617  odd2np1lem  15685  sqoddm1div8z  15699  ltoddhalfle  15706  halfleoddlt  15707  flodddiv4  15758  dvdssqim  15898  coprmdvds2  15992  divgcdcoprm0  16003  cncongr1  16005  cncongr2  16006  isprm5  16045  rpexp  16058  pythagtriplem1  16147  iserodd  16166  pc2dvds  16209  difsqpwdvds  16217  oddprmdvds  16233  prmpwdvds  16234  4sqlem11  16285  vdwapun  16304  vdwlem2  16312  vdwlem6  16316  vdwlem8  16318  vdwlem10  16320  vdwnnlem1  16325  vdwnnlem3  16327  0ram  16350  ramub1lem2  16357  ramcl  16359  cshwsiun  16429  cshwrepswhash1  16432  firest  16702  imasvscafn  16806  imasmnd2  17944  dfgrp3lem  18193  imasgrp2  18210  issubg4  18294  cycsubm  18341  gaorber  18434  orbsta  18439  pmtr3ncom  18599  psgnran  18639  odmulg  18679  odbezout  18681  gexdvdsi  18704  sylow1lem3  18721  odcau  18725  sylow2alem1  18738  sylow3lem6  18753  lsmelvalm  18772  efgrelexlemb  18872  efgredeu  18874  cyggeninv  18999  cygctb  19009  cyggexb  19016  dprdssv  19135  dprddisj2  19158  ablfacrplem  19184  pgpfac1lem2  19194  pgpfac1lem5  19198  ringinvnzdiv  19343  imasring  19369  dvdsrcl2  19400  dvdsrmul1  19403  lss1d  19732  lssats2  19769  lspsn  19771  lmhmima  19816  lpiss  20020  dvdsrzring  20180  znunit  20259  znrrg  20261  cygznlem3  20265  frgpcyg  20269  lindfrn  20514  mplcoe5lem  20711  mpfind  20783  gsummoncoe1  20937  mpfpf1  20979  pf1mpf  20980  mat1dimelbas  21080  scmatdmat  21124  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  cpmatacl  21325  chpscmat  21451  tgcl  21578  clsval2  21659  innei  21734  restcld  21781  restcldr  21783  ordtrest2lem  21812  cnprest  21898  lmss  21907  lmcls  21911  lmcnp  21913  isreg2  21986  cmpcovf  22000  cncmp  22001  cmpsub  22009  1stcrest  22062  2ndcrest  22063  1stccnp  22071  restnlly  22091  cldllycmp  22104  locfincmp  22135  txcnpi  22217  pthaus  22247  txtube  22249  txcmplem1  22250  txcmplem2  22251  txlm  22257  xkohaus  22262  xkococnlem  22268  xkococn  22269  kqfvima  22339  kqreglem1  22350  isfild  22467  filuni  22494  isufil2  22517  uffix  22530  rnelfm  22562  fmfnfmlem2  22564  fmfnfmlem4  22566  fmfnfm  22567  fmco  22570  fclsopn  22623  ufilcmp  22641  cnpfcf  22650  alexsublem  22653  alexsubALT  22660  cldsubg  22720  ghmcnp  22724  qustgpopn  22729  tsmsgsum  22748  tsmsres  22753  tsmsxplem1  22762  tsmsxp  22764  isucn2  22889  ucnprima  22892  imasdsf1olem  22984  blssps  23035  blss  23036  blssexps  23037  blssex  23038  mopni3  23105  blcld  23116  metrest  23135  metcnp3  23151  reperflem  23427  icccmplem3  23433  xrge0tsms  23443  mulc1cncf  23514  cncfco  23516  cnheibor  23564  bndth  23567  lebnumlem3  23572  xlebnum  23574  lebnumii  23575  nmhmcn  23729  cfil3i  23877  cmetcaulem  23896  cfilres  23904  bcthlem4  23935  ivthlem2  24060  ivthlem3  24061  ivthicc  24066  cniccbdd  24069  ovolunlem1  24105  ovoliunlem2  24111  ovolshftlem2  24118  ovolicc2  24130  iunmbl2  24165  dyadmax  24206  opnmbllem  24209  subopnmbl  24212  volivth  24215  ismbf3d  24262  mbfimaopn2  24265  mbfaddlem  24268  i1fmullem  24302  mbfi1fseqlem4  24326  bddiblnc  24449  ellimc3  24486  dvlip  24600  dvlip2  24602  c1liplem1  24603  dvgt0lem1  24609  dvivthlem2  24616  dvne0  24618  lhop1lem  24620  lhop2  24622  lhop  24623  tdeglem4  24665  mdegnn0cl  24676  ply1divex  24741  dvdsq1p  24765  ig1peu  24776  elply2  24797  plypf1  24813  plydivex  24897  aalioulem3  24934  aalioulem5  24936  aaliou  24938  ulmshftlem  24988  ulmcau  24994  ulmss  24996  ulmbdd  24997  ulmcn  24998  radcnvlt1  25017  eflogeq  25197  efopn  25253  cxpeq  25350  angpieqvd  25421  xrlimcnp  25558  cxploglim  25567  ftalem2  25663  ftalem7  25668  isppw2  25704  dchrptlem1  25852  dchrptlem3  25854  dchrsum2  25856  lgsdchrval  25942  lgsdchr  25943  gausslemma2dlem1a  25953  lgsquadlem1  25968  2lgsoddprmlem2  25997  dchrisumlem3  26079  dchrisum0fno1  26099  pntlem3  26197  pntleml  26199  ostth3  26226  brcgr  26698  brbtwn2  26703  axbtwnid  26737  axcontlem7  26768  usgrnloopALT  26997  uhgrspansubgrlem  27084  nbuhgr  27137  nbupgr  27138  wwlksnextprop  27702  elwspths2on  27750  erclwwlktr  27811  clwwlknscsh  27851  erclwwlkntr  27860  hashecclwwlkn1  27866  umgrhashecclwwlk  27867  3cyclfrgrrn1  28074  frgrregorufr  28114  frgr2wwlk1  28118  ubthlem1  28657  ubthlem3  28659  htthlem  28704  omlsii  29190  spansncol  29355  nmopun  29801  nmcexi  29813  riesz1  29852  elpjrn  29977  cvcon3  30071  chcv1  30142  atcvatlem  30172  chirredi  30181  br8d  30378  xrge0tsmsd  30746  ordtrest2NEWlem  31279  lmxrge0  31309  esumfsup  31443  esumpcvgval  31451  measdivcstALTV  31598  eulerpartlemgh  31750  dstfrvunirn  31846  afsval  32056  erdszelem8  32559  erdszelem11  32562  erdsze2lem2  32565  connpconn  32596  sconnpi1  32600  cvmsss2  32635  cvmfolem  32640  cvmliftmolem2  32643  cvmliftlem15  32659  cvmlift2lem1  32663  cvmlift3lem4  32683  cvmlift3lem5  32684  satfdmlem  32729  fmla1  32748  gonarlem  32755  gonar  32756  goalrlem  32757  goalr  32758  fmla0disjsuc  32759  fmlasucdisj  32760  satffunlem1lem1  32763  satffunlem1lem2  32764  satffunlem2lem1  32765  mrsub0  32877  mrsubcn  32880  msubrn  32890  msubvrs  32921  dvdspw  33096  br8  33106  br6  33107  br4  33108  nosupno  33317  nosupbday  33319  scutun12  33385  cgrtriv  33577  btwntriv2  33587  btwncomim  33588  btwnswapid  33592  btwnintr  33594  btwnexch3  33595  btwnouttr2  33597  ifscgr  33619  cgrxfr  33630  btwnxfr  33631  btwnconn3  33678  segcon2  33680  brsegle  33683  seglecgr12im  33685  broutsideof3  33701  linethru  33728  elhf2  33750  opnregcld  33792  cldregopn  33793  neibastop2lem  33822  matunitlindflem1  35052  poimirlem16  35072  poimirlem17  35073  poimirlem19  35075  poimirlem20  35076  poimirlem24  35080  poimirlem29  35085  heicant  35091  opnmbllem0  35092  ismblfin  35097  itg2addnclem  35107  itg2addnclem3  35109  itg2gt0cn  35111  ftc1anclem5  35133  ftc2nc  35138  filbcmb  35177  fdc  35182  incsequz  35185  caushft  35198  istotbnd3  35208  equivbnd  35227  cntotbnd  35233  heibor1lem  35246  heibor1  35247  bfplem2  35260  divrngidl  35465  prnc  35504  lshpdisj  36282  cvrcon3b  36572  atnle  36612  hlhgt2  36684  hl0lt1N  36685  hl2at  36700  cvrexchlem  36714  cvratlem  36716  lvolnlelpln  36880  2lplnj  36915  ispsubcl2N  37242  lautcvr  37387  dva1dim  38280  dib1dim  38460  dib1dim2  38463  diclspsn  38489  dih1dimatlem  38624  dihlatat  38632  dihatexv  38633  dihatexv2  38634  lcfrlem9  38845  lcfrlem16  38853  mapdrvallem2  38940  mapd1o  38943  elre0re  39455  dvdsexpim  39482  dffltz  39608  rexlimdv3d  39617  elrfi  39628  isnacs3  39644  eldiophb  39691  eldiophss  39708  diophren  39747  rencldnfilem  39754  pell1234qrdich  39795  pellfundex  39820  lsmfgcl  40011  kercvrlsm  40020  lmhmfgima  40021  lpirlnr  40054  hbtlem2  40061  hbtlem4  40063  hbtlem6  40066  rngunsnply  40110  restuni3  41746  limsupubuz  42348  stoweidlem57  42692  fourierdlem48  42789  fourierdlem49  42790  sge0le  43039  euoreqb  43658  imasetpreimafvbijlemf1  43914  imasetpreimafvbijlemfo  43915  iccpartrn  43940  iccpartiun  43944  iccpartnel  43948  paireqne  44021  reupr  44032  odz2prm2pw  44073  fmtnofac2lem  44078  prmdvdsfmtnof1lem2  44095  2pwp1prm  44099  mod42tp1mod8  44113  lighneallem3  44118  lighneallem4  44121  requad01  44132  requad2  44134  fppr2odd  44242  gbowpos  44270  gbowgt5  44273  gboge9  44275  nnsum4primesodd  44307  nnsum4primesoddALTV  44308  isomushgr  44337  isomuspgrlem2d  44342  copisnmnd  44422  lidldomn1  44538  affinecomb1  45109  eenglngeehlnmlem2  45145  rrx2vlinest  45148  itsclquadb  45183  aacllem  45322
  Copyright terms: Public domain W3C validator