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

Theorem exlimdv 1932
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 nfv 1629 . 2  |-  F/ x ph
2 nfv 1629 . 2  |-  F/ x ch
3 exlimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3exlimd 1784 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  ax11v2  1935  ax11v2-o  1936  exlimdvv  2026  ax11eq  2105  ax11el  2106  ax11inda  2113  tpid3g  3645  sssn  3672  euotd  4160  wefrc  4280  wereu2  4283  onfr  4324  reusv2lem2  4427  ralxfr2d  4441  releldmb  4820  relelrnb  4821  elres  4897  iss  4905  soex  5029  dffv2  5444  fvmptdv2  5465  dff3  5525  elunirnALT  5631  isomin  5686  isofrlem  5689  f1oweALT  5703  ovmpt4g  5822  op1steq  6016  reldmtpos  6094  rntpos  6099  tfrlem9a  6288  erref  6566  erdisj  6593  map0g  6693  resixpfo  6740  domdifsn  6830  xpdom2  6842  xpdom3  6845  domunsncan  6847  domunsn  6896  fodomr  6897  mapdom1  6911  mapdom2  6917  mapdom3  6918  phplem4  6928  php3  6932  sucdom2  6942  fineqvlem  6962  pssnn  6966  ssfi  6968  domfi  6969  findcard2  6983  ac6sfi  6986  isfinite2  7000  xpfi  7013  domunfican  7014  fiint  7018  fodomfib  7021  fissuni  7044  fipreima  7045  indexfi  7047  marypha1lem  7070  ordiso  7115  hartogslem1  7141  brwdom2  7171  wdomtr  7173  brwdom3  7180  unwdomg  7182  xpwdomg  7183  unxpwdom2  7186  unxpwdom  7187  inf3lem2  7214  infdifsn  7241  epfrs  7297  tcmin  7310  cplem1  7443  isinffi  7509  pm54.43  7517  dfac8alem  7540  dfac8b  7542  dfac8clem  7543  ac10ct  7545  ac5num  7547  acni2  7557  numacn  7560  acndom  7562  acndom2  7565  fodomacn  7567  numwdom  7570  wdomfil  7572  wdomnumr  7575  iunfictbso  7625  dfac2  7641  dfac9  7646  kmlem13  7672  cdainf  7702  infpss  7727  fictb  7755  cfeq0  7766  cff1  7768  cfflb  7769  cofsmo  7779  cfsmolem  7780  coftr  7783  infpssr  7818  fin4en1  7819  ssfin4  7820  domfin4  7821  fin23lem7  7826  enfin2i  7831  fin23lem31  7853  fin23lem41  7862  isf34lem4  7887  axcc3  7948  domtriomlem  7952  axdc2lem  7958  axdc3lem2  7961  axdc3lem4  7963  axdc4lem  7965  axcclem  7967  ac6num  7990  ttukeylem6  8025  ttukeyg  8028  fodomb  8035  iundom2g  8046  alephreg  8084  fpwwe2lem11  8142  fpwwe2lem12  8143  canthp1lem1  8154  canthp1  8156  pwfseq  8166  winafp  8199  wun0  8220  gruen  8314  grudomon  8319  gruina  8320  grur1  8322  ltexnq  8479  ltbtwnnq  8482  genpn0  8507  psslinpr  8535  prlem934  8537  ltaddpr  8538  ltexprlem2  8541  ltexprlem6  8545  ltexprlem7  8546  prlem936  8551  reclem2pr  8552  reclem4pr  8554  suplem1pr  8556  sup2  9590  supmul1  9599  supmul  9602  infmrcl  9613  negn0  10183  zsupss  10186  supxrre  10524  infmxrre  10532  ixxub  10555  ixxlb  10556  hashfun  11266  hashf1  11272  rlimdm  11902  climcau  12021  caucvgb  12029  summolem2  12066  zsum  12068  sumz  12072  fsumf1o  12073  fsumss  12075  fsumcl2lem  12081  fsumadd  12088  fsummulc2  12123  fsumconst  12129  fsumrelem  12142  isumltss  12181  ruclem13  12394  eulerth  12725  4sqlem12  12877  vdwapun  12895  vdwlem9  12910  vdwlem10  12911  ramub2  12935  ramz  12946  ramub1  12949  firest  13211  mremre  13378  isacs2  13400  iscatd2  13427  sscfn1  13538  sscfn2  13539  gsumval2a  14294  issubg2  14471  sylow1lem4  14747  sylow3  14779  prmcyg  15015  cyggex2  15018  gsumval3  15026  gsumzres  15029  gsumzcl  15030  gsumzf1o  15031  gsumzaddlem  15038  gsumconst  15044  gsumzmhm  15045  gsumzoppg  15051  gsum2d2  15060  pgpfac1lem5  15149  ablfaclem3  15157  lss0cl  15539  lbspss  15670  lsmcv  15729  lspsnat  15732  cnsubrg  16264  gsumfsum  16271  cygzn  16356  obslbs  16462  eltg3  16532  tgtop  16543  tgidm  16550  ppttop  16576  toponmre  16662  tgrest  16722  tgcn  16814  lmff  16861  cmpsublem  16958  cmpsub  16959  tgcmp  16960  hauscmplem  16965  iunconlem  16985  uncon  16987  clscon  16988  1stcfb  17003  2ndcctbss  17013  2ndcdisj  17014  2ndcsep  17017  1stcelcls  17019  1stccnp  17020  1stckgen  17081  ptuni2  17103  ptbasfi  17108  ptpjopn  17138  ptclsg  17141  ptcnplem  17147  ptcnp  17148  txcn  17152  prdstopn  17154  txindis  17160  txtube  17166  txcmplem1  17167  txcmplem2  17168  xkococnlem  17185  txcon  17215  fbdmn0  17361  trfbas2  17370  filtop  17382  filcon  17410  filssufilg  17438  fmfnfm  17485  ufldom  17489  hauspwpwf1  17514  alexsubALTlem3  17575  alexsubALT  17577  ptcmplem2  17579  ptcmplem3  17580  tmdgsum2  17611  tgptsmscld  17665  tsmsxplem1  17667  xbln0  17797  met2ndci  17900  nmoid  18083  opnreen  18168  metdsre  18189  cnheibor  18285  phtpcer  18325  phtpc01  18326  phtpcco2  18329  cfilfcls  18532  cmetcaulem  18546  cmetcau  18547  iscmet3lem2  18550  iscmet3  18551  bcthlem4  18581  bcthlem5  18582  ovolctb  18681  ovoliunlem3  18695  ovoliunnul  18698  ovolicc2lem2  18709  ovolicc2lem5  18712  ovolicc2  18713  dyadmbl  18787  vitali  18800  mbfimaopnlem  18842  itg11  18878  bddmulibl  19025  limciun  19076  perfdvf  19085  dvcnp2  19101  dvlip  19172  dvne0  19190  fta1g  19385  fta1  19520  vieta1lem2  19523  ulmcau  19604  pserulm  19630  wilthlem2  20139  dchrvmasumif  20484  rpvmasum2  20493  dchrisum0re  20494  dchrisum0lem3  20500  dchrisum0  20501  dchrmusum  20505  dchrvmasum  20506  isgrp2d  20732  minvecolem5  21290  spansncvi  22079  derangenlem  22873  erdsze2lem1  22905  erdsze2  22907  ptpcon  22935  cvmsss2  22976  cvmopnlem  22980  cvmfolem  22981  cvmliftmolem2  22984  cvmliftlem15  23000  cvmlift2lem10  23014  cvmliftpht  23020  cvmlift3lem8  23028  rtrclreclem.trans  23214  fundmpss  23290  frmin  23410  wfrlem12  23435  frrlem11  23461  nocvxmin  23513  axcontlem10  23775  injrec2  24285  surjsec2  24286  dffprod  24485  fnessref  25459  refssfne  25460  locfincmp  25470  comppfsc  25473  neibastop2lem  25475  neibastop2  25476  fnemeet2  25482  fnejoin2  25484  tailfb  25492  filnetlem3  25495  sdclem1  25619  fdc  25621  istotbnd3  25661  sstotbnd2  25664  sstotbnd  25665  prdsbnd  25683  prdstotbnd  25684  prdsbnd2  25685  heibor1lem  25699  heiborlem1  25701  heiborlem10  25710  heibor  25711  bfp  25714  riscer  25785  divrngidl  25819  prtlem17  25910  eldioph2lem1  26005  eldioph2lem2  26006  rencldnfilem  26069  kelac1  26327  enfixsn  26423  mapfien2  26424  lmiclbs  26473  lbslcic  26477  lmisfree  26478  hbt  26500  symggen  26577  psgnunilem3  26585  cncmpmax  26870  stoweidlem28  26911  stoweidlem31  26914  stoweidlem43  26926  stoweidlem46  26929  stoweidlem48  26931  stoweidlem56  26939  stoweidlem57  26940  stoweidlem59  26942  stoweidlem60  26943  onfrALT  27104  bnj849  27743  llnn0  28609  lplnn0N  28640  lvoln0N  28684  osumcllem8N  29056  pexmidlem5N  29067  diaglbN  30149  diaintclN  30152  dibglbN  30260  dibintclN  30261  dihglblem2aN  30387  dihintcl  30438  dvh1dim  30536  mapdrvallem2  30739
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator