MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimdv Unicode version

Theorem exlimdv 1646
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. Revised to remove dependency on ax-9 1666 and ax-8 1687. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen, 4-Dec-2017.)
Hypothesis
Ref Expression
exlimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
exlimdv  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimdv
StepHypRef Expression
1 exlimdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21eximdv 1632 . 2  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
3 ax17e 1628 . 2  |-  ( E. x ch  ->  ch )
42, 3syl6 31 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  exlimdvv  1647  exlimddv  1648  ax10OLD  2032  ax11v2  2074  ax11v2OLD  2075  ax11eq  2269  ax11el  2270  ax11inda  2276  ax11v2-o  2277  tpid3g  3911  sssn  3949  euotd  4449  wefrc  4568  wereu2  4571  onfr  4612  reusv2lem2  4716  ralxfr2d  4730  releldmb  5095  relelrnb  5096  elres  5172  iss  5180  soex  5310  dffv2  5787  dff3  5873  elunirnALT  5991  isomin  6048  isofrlem  6051  f1oweALT  6065  ovmpt4g  6187  op1steq  6382  fo2ndf  6444  mpt2xopynvov0g  6456  reldmtpos  6478  rntpos  6483  erdisj  6943  map0g  7044  resixpfo  7091  domdifsn  7182  xpdom3  7197  domunsncan  7199  fodomr  7249  mapdom2  7269  mapdom3  7270  phplem4  7280  php3  7284  sucdom2  7294  pssnn  7318  ssfi  7320  domfi  7321  findcard2  7339  ac6sfi  7342  isfinite2  7356  xpfi  7369  domunfican  7370  fiint  7374  fodomfib  7377  marypha1lem  7429  ordiso  7474  hartogslem1  7500  brwdom2  7530  wdomtr  7532  brwdom3  7539  unwdomg  7541  xpwdomg  7542  unxpwdom2  7545  inf3lem2  7573  epfrs  7656  tcmin  7669  cplem1  7802  pm54.43  7876  dfac8alem  7899  dfac8b  7901  dfac8clem  7902  ac10ct  7904  acni2  7916  acndom  7921  numwdom  7929  wdomfil  7931  wdomnumr  7934  iunfictbso  7984  dfac2  8000  dfac9  8005  kmlem13  8031  cdainf  8061  fictb  8114  cfeq0  8125  cff1  8127  cfflb  8128  cofsmo  8138  cfsmolem  8139  coftr  8142  infpssr  8177  fin4en1  8178  fin23lem7  8185  isf34lem4  8246  axcc3  8307  domtriomlem  8311  axdc2lem  8317  axdc3lem2  8320  axdc3lem4  8322  axdc4lem  8324  ac6num  8348  ttukeylem6  8383  ttukeyg  8386  fodomb  8393  iundom2g  8404  alephreg  8446  fpwwe2lem11  8504  fpwwe2lem12  8505  canthp1  8518  pwfseq  8528  gruen  8676  grudomon  8681  gruina  8682  grur1  8684  ltexnq  8841  ltbtwnnq  8844  genpn0  8869  psslinpr  8897  prlem934  8899  ltaddpr  8900  ltexprlem2  8903  ltexprlem6  8907  ltexprlem7  8908  reclem2pr  8914  reclem4pr  8916  suplem1pr  8918  sup2  9953  supmul1  9962  infmrcl  9976  negn0  10551  zsupss  10554  fiinfnf1o  11622  hashfun  11688  hashf1  11694  rlimdm  12333  climcau  12452  caucvgb  12461  summolem2  12498  zsum  12500  sumz  12504  fsumf1o  12505  fsumss  12507  fsumcl2lem  12513  fsumadd  12520  fsummulc2  12555  fsumconst  12561  fsumrelem  12574  ruclem13  12829  4sqlem12  13312  vdwapun  13330  vdwlem9  13345  vdwlem10  13346  ramz  13381  ramub1  13384  firest  13648  mremre  13817  isacs2  13866  iscatd2  13894  sscfn1  14005  sscfn2  14006  gsumval2a  14770  cyggex2  15494  gsumval3  15502  gsumzres  15505  gsumzcl  15506  gsumzf1o  15507  gsumzaddlem  15514  gsumconst  15520  gsumzmhm  15521  gsumzoppg  15527  gsum2d2  15536  pgpfac1lem5  15625  ablfaclem3  15633  lss0cl  16011  lspsnat  16205  cnsubrg  16747  gsumfsum  16754  obslbs  16945  eltg3  17015  tgtop  17026  tgidm  17033  ppttop  17059  toponmre  17145  tgrest  17211  neitr  17232  tgcn  17304  cmpsublem  17450  cmpsub  17451  iunconlem  17478  uncon  17480  1stcfb  17496  2ndcctbss  17506  2ndcdisj  17507  1stcelcls  17512  1stccnp  17513  1stckgen  17574  ptuni2  17596  ptbasfi  17601  ptpjopn  17632  ptclsg  17635  ptcnp  17642  prdstopn  17648  txindis  17654  txtube  17660  txcmplem1  17661  txcmplem2  17662  xkococnlem  17679  txcon  17709  trfbas2  17863  filtop  17875  filcon  17903  filssufilg  17931  fmfnfm  17978  ufldom  17982  hauspwpwf1  18007  alexsubALTlem3  18068  alexsubALT  18070  ptcmplem2  18072  tmdgsum2  18114  tgptsmscld  18168  ustfilxp  18230  xbln0  18432  opnreen  18850  metdsre  18871  cnheibor  18968  phtpc01  19009  cfilfcls  19215  cmetcaulem  19229  iscmet3  19234  ovolctb  19374  ovoliunlem3  19388  ovoliunnul  19391  ovolicc2lem5  19405  ovolicc2  19406  dyadmbl  19480  vitali  19493  itg11  19571  bddmulibl  19718  perfdvf  19778  dvcnp2  19794  dvlip  19865  dvne0  19883  fta1g  20078  fta1  20213  ulmcau  20299  pserulm  20326  wilthlem2  20840  dchrvmasumif  21185  rpvmasum2  21194  dchrisum0re  21195  dchrisum0lem3  21201  dchrisum0  21202  dchrmusum  21206  dchrvmasum  21207  usgrafisindb1  21411  spansncvi  23142  fmcncfil  24305  volmeas  24575  derangenlem  24845  cvmsss2  24949  cvmopnlem  24953  cvmfolem  24954  cvmliftmolem2  24957  cvmliftlem15  24973  cvmlift2lem10  24987  cvmlift3lem8  25001  rtrclreclem.trans  25134  ntrivcvg  25214  prodmolem2  25250  zprod  25252  prod1  25259  fprodf1o  25261  fprodss  25263  fprodcl2lem  25265  fprodmul  25273  fproddiv  25274  fprodconst  25291  fprodn0  25292  fundmpss  25377  frmin  25497  wfrlem12  25522  frrlem11  25548  nocvxmin  25600  axcontlem10  25860  supaddc  26184  itg2addnclem  26202  fnessref  26310  refssfne  26311  locfincmp  26321  comppfsc  26324  neibastop2lem  26326  neibastop2  26327  fnemeet2  26333  fnejoin2  26335  tailfb  26343  sdclem1  26384  fdc  26386  istotbnd3  26417  sstotbnd2  26420  prdsbnd2  26441  heibor1lem  26455  heiborlem1  26457  heiborlem10  26466  heibor  26467  riscer  26541  divrngidl  26575  prtlem17  26662  enfixsn  27172  mapfien2  27173  lmiclbs  27222  lmisfree  27227  symggen  27326  stoweidlem43  27706  stoweidlem48  27711  stoweidlem57  27720  stoweidlem60  27723  rlimdmafv  27955  frgra3vlem2  28249  onfrALT  28490  chordthmALT  28900  bnj849  29150  ax10NEW7  29327  ax11v2NEW7  29382  osumcllem8N  30599  pexmidlem5N  30610  mapdrvallem2  32282
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator