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

Theorem exlimdv 1665
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
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 1609 . 2  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
3 19.9v 1664 . 2  |-  ( E. x ch  <->  ch )
42, 3syl6ib 219 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1529
This theorem is referenced by:  exlimddv  1666  exlimdvv  1669  ax10  1885  ax11v2  1935  ax11eq  2133  ax11el  2134  ax11inda  2140  ax11v2-o  2141  tpid3g  3742  sssn  3773  euotd  4266  wefrc  4386  wereu2  4389  onfr  4430  reusv2lem2  4535  ralxfr2d  4549  releldmb  4912  relelrnb  4913  elres  4989  iss  4997  soex  5121  dffv2  5553  fvmptdv2  5574  dff3  5634  elunirnALT  5740  isomin  5795  isofrlem  5798  f1oweALT  5812  ovmpt4g  5931  op1steq  6125  reldmtpos  6203  rntpos  6208  tfrlem9a  6397  erref  6675  erdisj  6702  map0g  6802  resixpfo  6849  domdifsn  6940  xpdom2  6952  xpdom3  6955  domunsncan  6957  domunsn  7006  fodomr  7007  mapdom1  7021  mapdom2  7027  mapdom3  7028  phplem4  7038  php3  7042  sucdom2  7052  fineqvlem  7072  pssnn  7076  ssfi  7078  domfi  7079  findcard2  7093  ac6sfi  7096  isfinite2  7110  xpfi  7123  domunfican  7124  fiint  7128  fodomfib  7131  fissuni  7155  fipreima  7156  indexfi  7158  marypha1lem  7181  ordiso  7226  hartogslem1  7252  brwdom2  7282  wdomtr  7284  brwdom3  7291  unwdomg  7293  xpwdomg  7294  unxpwdom2  7297  unxpwdom  7298  inf3lem2  7325  infdifsn  7352  epfrs  7408  tcmin  7421  cplem1  7554  isinffi  7620  pm54.43  7628  dfac8alem  7651  dfac8b  7653  dfac8clem  7654  ac10ct  7656  ac5num  7658  acni2  7668  numacn  7671  acndom  7673  acndom2  7676  fodomacn  7678  numwdom  7681  wdomfil  7683  wdomnumr  7686  iunfictbso  7736  dfac2  7752  dfac9  7757  kmlem13  7783  cdainf  7813  infpss  7838  fictb  7866  cfeq0  7877  cff1  7879  cfflb  7880  cofsmo  7890  cfsmolem  7891  coftr  7894  infpssr  7929  fin4en1  7930  ssfin4  7931  domfin4  7932  fin23lem7  7937  enfin2i  7942  fin23lem31  7964  fin23lem41  7973  isf34lem4  7998  axcc3  8059  domtriomlem  8063  axdc2lem  8069  axdc3lem2  8072  axdc3lem4  8074  axdc4lem  8076  axcclem  8078  ac6num  8101  ttukeylem6  8136  ttukeyg  8139  fodomb  8146  iundom2g  8157  alephreg  8199  fpwwe2lem11  8257  fpwwe2lem12  8258  canthp1lem1  8269  canthp1  8271  pwfseq  8281  winafp  8314  wun0  8335  gruen  8429  grudomon  8434  gruina  8435  grur1  8437  ltexnq  8594  ltbtwnnq  8597  genpn0  8622  psslinpr  8650  prlem934  8652  ltaddpr  8653  ltexprlem2  8656  ltexprlem6  8660  ltexprlem7  8661  prlem936  8666  reclem2pr  8667  reclem4pr  8669  suplem1pr  8671  sup2  9705  supmul1  9714  supmul  9717  infmrcl  9728  negn0  10299  zsupss  10302  supxrre  10640  infmxrre  10648  ixxub  10671  ixxlb  10672  hashfun  11383  hashf1  11389  rlimdm  12019  climcau  12138  caucvgb  12146  summolem2  12183  zsum  12185  sumz  12189  fsumf1o  12190  fsumss  12192  fsumcl2lem  12198  fsumadd  12205  fsummulc2  12240  fsumconst  12246  fsumrelem  12259  isumltss  12301  ruclem13  12514  eulerth  12845  4sqlem12  12997  vdwapun  13015  vdwlem9  13030  vdwlem10  13031  ramub2  13055  ramz  13066  ramub1  13069  firest  13331  mremre  13500  isacs2  13549  iscatd2  13577  sscfn1  13688  sscfn2  13689  gsumval2a  14453  issubg2  14630  sylow1lem4  14906  sylow3  14938  prmcyg  15174  cyggex2  15177  gsumval3  15185  gsumzres  15188  gsumzcl  15189  gsumzf1o  15190  gsumzaddlem  15197  gsumconst  15203  gsumzmhm  15204  gsumzoppg  15210  gsum2d2  15219  pgpfac1lem5  15308  ablfaclem3  15316  lss0cl  15698  lbspss  15829  lsmcv  15888  lspsnat  15892  cnsubrg  16426  gsumfsum  16433  cygzn  16518  obslbs  16624  eltg3  16694  tgtop  16705  tgidm  16712  ppttop  16738  toponmre  16824  tgrest  16884  tgcn  16976  lmff  17023  cmpsublem  17120  cmpsub  17121  tgcmp  17122  hauscmplem  17127  iunconlem  17147  uncon  17149  clscon  17150  1stcfb  17165  2ndcctbss  17175  2ndcdisj  17176  2ndcsep  17179  1stcelcls  17181  1stccnp  17182  1stckgen  17243  ptuni2  17265  ptbasfi  17270  ptpjopn  17300  ptclsg  17303  ptcnplem  17309  ptcnp  17310  txcn  17314  prdstopn  17316  txindis  17322  txtube  17328  txcmplem1  17329  txcmplem2  17330  xkococnlem  17347  txcon  17377  fbdmn0  17523  trfbas2  17532  filtop  17544  filcon  17572  filssufilg  17600  fmfnfm  17647  ufldom  17651  hauspwpwf1  17676  alexsubALTlem3  17737  alexsubALT  17739  ptcmplem2  17741  ptcmplem3  17742  tmdgsum2  17773  tgptsmscld  17827  tsmsxplem1  17829  xbln0  17959  met2ndci  18062  nmoid  18245  opnreen  18330  metdsre  18351  cnheibor  18447  phtpcer  18487  phtpc01  18488  phtpcco2  18491  cfilfcls  18694  cmetcaulem  18708  cmetcau  18709  iscmet3lem2  18712  iscmet3  18713  bcthlem4  18743  bcthlem5  18744  ovolctb  18843  ovoliunlem3  18857  ovoliunnul  18860  ovolicc2lem2  18871  ovolicc2lem5  18874  ovolicc2  18875  dyadmbl  18949  vitali  18962  mbfimaopnlem  19004  itg11  19040  bddmulibl  19187  limciun  19238  perfdvf  19247  dvcnp2  19263  dvlip  19334  dvne0  19352  fta1g  19547  fta1  19682  vieta1lem2  19685  ulmcau  19766  pserulm  19792  wilthlem2  20301  dchrvmasumif  20646  rpvmasum2  20655  dchrisum0re  20656  dchrisum0lem3  20662  dchrisum0  20663  dchrmusum  20667  dchrvmasum  20668  isgrp2d  20894  minvecolem5  21452  spansncvi  22223  derangenlem  23106  erdsze2lem1  23138  erdsze2  23140  ptpcon  23168  cvmsss2  23209  cvmopnlem  23213  cvmfolem  23214  cvmliftmolem2  23217  cvmliftlem15  23233  cvmlift2lem10  23247  cvmliftpht  23253  cvmlift3lem8  23261  rtrclreclem.trans  23447  fundmpss  23523  frmin  23643  wfrlem12  23668  frrlem11  23694  nocvxmin  23746  axcontlem10  24008  injrec2  24518  surjsec2  24519  dffprod  24718  fnessref  25692  refssfne  25693  locfincmp  25703  comppfsc  25706  neibastop2lem  25708  neibastop2  25709  fnemeet2  25715  fnejoin2  25717  tailfb  25725  filnetlem3  25728  sdclem1  25852  fdc  25854  istotbnd3  25894  sstotbnd2  25897  sstotbnd  25898  prdsbnd  25916  prdstotbnd  25917  prdsbnd2  25918  heibor1lem  25932  heiborlem1  25934  heiborlem10  25943  heibor  25944  bfp  25947  riscer  26018  divrngidl  26052  prtlem17  26143  eldioph2lem1  26238  eldioph2lem2  26239  rencldnfilem  26302  kelac1  26560  enfixsn  26656  mapfien2  26657  lmiclbs  26706  lbslcic  26710  lmisfree  26711  hbt  26733  symggen  26810  psgnunilem3  26818  cncmpmax  27102  stoweidlem28  27176  stoweidlem31  27179  stoweidlem43  27191  stoweidlem46  27194  stoweidlem48  27196  stoweidlem56  27204  stoweidlem57  27205  stoweidlem59  27207  stoweidlem60  27208  onfrALT  27585  bnj849  28224  llnn0  28972  lplnn0N  29003  lvoln0N  29047  osumcllem8N  29419  pexmidlem5N  29430  diaglbN  30512  diaintclN  30515  dibglbN  30623  dibintclN  30624  dihglblem2aN  30750  dihintcl  30801  dvh1dim  30899  mapdrvallem2  31102
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530
  Copyright terms: Public domain W3C validator