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

Theorem exlimdv 1664
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 1608 . 2  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
3 19.9v 1663 . 2  |-  ( E. x ch  <->  ch )
42, 3syl6ib 217 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  exlimddv  1665  exlimdvv  1668  ax10  1884  ax11v2  1932  ax11eq  2132  ax11el  2133  ax11inda  2139  ax11v2-o  2140  tpid3g  3741  sssn  3772  euotd  4267  wefrc  4387  wereu2  4390  onfr  4431  reusv2lem2  4536  ralxfr2d  4550  releldmb  4913  relelrnb  4914  elres  4990  iss  4998  soex  5122  dffv2  5592  fvmptdv2  5613  dff3  5673  elunirnALT  5779  isomin  5834  isofrlem  5837  f1oweALT  5851  ovmpt4g  5970  op1steq  6164  reldmtpos  6242  rntpos  6247  tfrlem9a  6402  erref  6680  erdisj  6707  map0g  6807  resixpfo  6854  domdifsn  6945  xpdom2  6957  xpdom3  6960  domunsncan  6962  domunsn  7011  fodomr  7012  mapdom1  7026  mapdom2  7032  mapdom3  7033  phplem4  7043  php3  7047  sucdom2  7057  fineqvlem  7077  pssnn  7081  ssfi  7083  domfi  7084  findcard2  7098  ac6sfi  7101  isfinite2  7115  xpfi  7128  domunfican  7129  fiint  7133  fodomfib  7136  fissuni  7160  fipreima  7161  indexfi  7163  marypha1lem  7186  ordiso  7231  hartogslem1  7257  brwdom2  7287  wdomtr  7289  brwdom3  7296  unwdomg  7298  xpwdomg  7299  unxpwdom2  7302  unxpwdom  7303  inf3lem2  7330  infdifsn  7357  epfrs  7413  tcmin  7426  cplem1  7559  isinffi  7625  pm54.43  7633  dfac8alem  7656  dfac8b  7658  dfac8clem  7659  ac10ct  7661  ac5num  7663  acni2  7673  numacn  7676  acndom  7678  acndom2  7681  fodomacn  7683  numwdom  7686  wdomfil  7688  wdomnumr  7691  iunfictbso  7741  dfac2  7757  dfac9  7762  kmlem13  7788  cdainf  7818  infpss  7843  fictb  7871  cfeq0  7882  cff1  7884  cfflb  7885  cofsmo  7895  cfsmolem  7896  coftr  7899  infpssr  7934  fin4en1  7935  ssfin4  7936  domfin4  7937  fin23lem7  7942  enfin2i  7947  fin23lem31  7969  fin23lem41  7978  isf34lem4  8003  axcc3  8064  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ac6num  8106  ttukeylem6  8141  ttukeyg  8144  fodomb  8151  iundom2g  8162  alephreg  8204  fpwwe2lem11  8262  fpwwe2lem12  8263  canthp1lem1  8274  canthp1  8276  pwfseq  8286  winafp  8319  wun0  8340  gruen  8434  grudomon  8439  gruina  8440  grur1  8442  ltexnq  8599  ltbtwnnq  8602  genpn0  8627  psslinpr  8655  prlem934  8657  ltaddpr  8658  ltexprlem2  8661  ltexprlem6  8665  ltexprlem7  8666  prlem936  8671  reclem2pr  8672  reclem4pr  8674  suplem1pr  8676  sup2  9710  supmul1  9719  supmul  9722  infmrcl  9733  negn0  10304  zsupss  10307  supxrre  10646  infmxrre  10654  ixxub  10677  ixxlb  10678  hashfun  11389  hashf1  11395  rlimdm  12025  climcau  12144  caucvgb  12152  summolem2  12189  zsum  12191  sumz  12195  fsumf1o  12196  fsumss  12198  fsumcl2lem  12204  fsumadd  12211  fsummulc2  12246  fsumconst  12252  fsumrelem  12265  isumltss  12307  ruclem13  12520  eulerth  12851  4sqlem12  13003  vdwapun  13021  vdwlem9  13036  vdwlem10  13037  ramub2  13061  ramz  13072  ramub1  13075  firest  13337  mremre  13506  isacs2  13555  iscatd2  13583  sscfn1  13694  sscfn2  13695  gsumval2a  14459  issubg2  14636  sylow1lem4  14912  sylow3  14944  prmcyg  15180  cyggex2  15183  gsumval3  15191  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  gsum2d2  15225  pgpfac1lem5  15314  ablfaclem3  15322  lss0cl  15704  lbspss  15835  lsmcv  15894  lspsnat  15898  cnsubrg  16432  gsumfsum  16439  cygzn  16524  obslbs  16630  eltg3  16700  tgtop  16711  tgidm  16718  ppttop  16744  toponmre  16830  tgrest  16890  tgcn  16982  lmff  17029  cmpsublem  17126  cmpsub  17127  tgcmp  17128  hauscmplem  17133  iunconlem  17153  uncon  17155  clscon  17156  1stcfb  17171  2ndcctbss  17181  2ndcdisj  17182  2ndcsep  17185  1stcelcls  17187  1stccnp  17188  1stckgen  17249  ptuni2  17271  ptbasfi  17276  ptpjopn  17306  ptclsg  17309  ptcnplem  17315  ptcnp  17316  txcn  17320  prdstopn  17322  txindis  17328  txtube  17334  txcmplem1  17335  txcmplem2  17336  xkococnlem  17353  txcon  17383  fbdmn0  17529  trfbas2  17538  filtop  17550  filcon  17578  filssufilg  17606  fmfnfm  17653  ufldom  17657  hauspwpwf1  17682  alexsubALTlem3  17743  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  tmdgsum2  17779  tgptsmscld  17833  tsmsxplem1  17835  xbln0  17965  met2ndci  18068  nmoid  18251  opnreen  18336  metdsre  18357  cnheibor  18453  phtpcer  18493  phtpc01  18494  phtpcco2  18497  cfilfcls  18700  cmetcaulem  18714  cmetcau  18715  iscmet3lem2  18718  iscmet3  18719  bcthlem4  18749  bcthlem5  18750  ovolctb  18849  ovoliunlem3  18863  ovoliunnul  18866  ovolicc2lem2  18877  ovolicc2lem5  18880  ovolicc2  18881  dyadmbl  18955  vitali  18968  mbfimaopnlem  19010  itg11  19046  bddmulibl  19193  limciun  19244  perfdvf  19253  dvcnp2  19269  dvlip  19340  dvne0  19358  fta1g  19553  fta1  19688  vieta1lem2  19691  ulmcau  19772  pserulm  19798  wilthlem2  20307  dchrvmasumif  20652  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  dchrmusum  20673  dchrvmasum  20674  isgrp2d  20902  minvecolem5  21460  spansncvi  22231  esumcst  23436  derangenlem  23702  erdsze2lem1  23734  erdsze2  23736  ptpcon  23764  cvmsss2  23805  cvmopnlem  23809  cvmfolem  23810  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem10  23843  cvmliftpht  23849  cvmlift3lem8  23857  rtrclreclem.trans  24043  fundmpss  24122  frmin  24242  wfrlem12  24267  frrlem11  24293  nocvxmin  24345  axcontlem10  24601  injrec2  25119  surjsec2  25120  dffprod  25319  fnessref  26293  refssfne  26294  locfincmp  26304  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  fnemeet2  26316  fnejoin2  26318  tailfb  26326  filnetlem3  26329  sdclem1  26453  fdc  26455  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  heibor1lem  26533  heiborlem1  26535  heiborlem10  26544  heibor  26545  bfp  26548  riscer  26619  divrngidl  26653  prtlem17  26744  eldioph2lem1  26839  eldioph2lem2  26840  rencldnfilem  26903  kelac1  27161  enfixsn  27257  mapfien2  27258  lmiclbs  27307  lbslcic  27311  lmisfree  27312  hbt  27334  symggen  27411  psgnunilem3  27419  cncmpmax  27703  stoweidlem28  27777  stoweidlem31  27780  stoweidlem43  27792  stoweidlem46  27795  stoweidlem48  27797  stoweidlem56  27805  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  mpt2xopynvov0g  28080  frgra3vlem2  28179  onfrALT  28314  chordthmALT  28710  bnj849  28957  llnn0  29705  lplnn0N  29736  lvoln0N  29780  osumcllem8N  30152  pexmidlem5N  30163  diaglbN  31245  diaintclN  31248  dibglbN  31356  dibintclN  31357  dihglblem2aN  31483  dihintcl  31534  dvh1dim  31632  mapdrvallem2  31835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator