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

Theorem exlimdv 2002
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2219. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 2046, ax-7 2082. (Revised by Wolf Lammen, 4-Dec-2017.)
Hypothesis
Ref Expression
exlimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exlimdv (𝜑 → (∃𝑥𝜓𝜒))
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv
StepHypRef Expression
1 exlimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21eximdv 1987 . 2 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3 ax5e 1982 . 2 (∃𝑥𝜒𝜒)
42, 3syl6 35 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980
This theorem depends on definitions:  df-bi 197  df-ex 1846
This theorem is referenced by:  exlimdvv  2003  exlimddv  2004  ax13lem1  2385  ax13  2386  nfeqf  2438  axc15  2440  sbcom2  2574  sssn  4495  elpreqprb  4540  reusv2lem2  5010  reusv2lem2OLD  5011  ralxfr2d  5023  euotd  5115  wefrc  5252  wereu2  5255  releldmb  5507  relelrnb  5508  elres  5585  iss  5597  onfr  5916  dffv2  6425  dff3  6527  elunirn  6664  fsnex  6693  f1prex  6694  isomin  6742  isofrlem  6745  ovmpt4g  6940  soex  7266  f1oweALT  7309  op1steq  7369  fo2ndf  7444  mpt2xopynvov0g  7501  reldmtpos  7521  rntpos  7526  wfrlem12  7587  wfrlem17  7592  erdisj  7953  map0g  8055  resixpfo  8104  domdifsn  8200  xpdom3  8215  domunsncan  8217  enfixsn  8226  fodomr  8268  mapdom2  8288  mapdom3  8289  phplem4  8299  php3  8303  sucdom2  8313  pssnn  8335  ssfi  8337  domfi  8338  findcard2  8357  ac6sfi  8361  isfinite2  8375  xpfi  8388  domunfican  8390  fiint  8394  fodomfib  8397  mapfien2  8471  marypha1lem  8496  ordiso  8578  hartogslem1  8604  brwdom2  8635  wdomtr  8637  brwdom3  8644  unwdomg  8646  xpwdomg  8647  unxpwdom2  8650  inf3lem2  8691  epfrs  8772  tcmin  8782  cplem1  8917  pm54.43  9008  dfac8alem  9034  dfac8b  9036  dfac8clem  9037  ac10ct  9039  acni2  9051  acndom  9056  numwdom  9064  wdomfil  9066  wdomnumr  9069  iunfictbso  9119  dfac2b  9135  dfac2OLD  9137  dfac9  9142  kmlem13  9168  cdainf  9198  fictb  9251  cfeq0  9262  cff1  9264  cfflb  9265  cofsmo  9275  cfsmolem  9276  coftr  9279  infpssr  9314  fin4en1  9315  fin23lem7  9322  isf34lem4  9383  axcc3  9444  domtriomlem  9448  axdc2lem  9454  axdc3lem2  9457  axdc3lem4  9459  axdc4lem  9461  ac6num  9485  ttukeylem6  9520  ttukeyg  9523  fodomb  9532  iundom2g  9546  alephreg  9588  fpwwe2lem11  9646  fpwwe2lem12  9647  canthp1  9660  pwfseq  9670  gruen  9818  grudomon  9823  gruina  9824  grur1  9826  ltexnq  9981  ltbtwnnq  9984  genpn0  10009  psslinpr  10037  prlem934  10039  ltaddpr  10040  ltexprlem2  10043  ltexprlem6  10047  ltexprlem7  10048  reclem2pr  10054  reclem4pr  10056  suplem1pr  10058  negn0  10643  sup2  11163  supaddc  11174  supmul1  11176  zsupss  11962  fiinfnf1o  13324  hasheqf1oi  13326  hashfun  13408  hashf1  13425  rtrclreclem3  13991  rlimdm  14473  climcau  14592  caucvgb  14601  summolem2  14638  zsum  14640  sumz  14644  fsumf1o  14645  fsumss  14647  fsumcl2lem  14653  fsumadd  14661  fsummulc2  14707  fsumconst  14713  fsumrelem  14730  ntrivcvg  14820  prodmolem2  14856  zprod  14858  prod1  14865  fprodf1o  14867  fprodss  14869  fprodcl2lem  14871  fprodmul  14881  fproddiv  14882  fprodconst  14899  fprodn0  14900  ruclem13  15162  4sqlem12  15854  vdwapun  15872  vdwlem9  15887  vdwlem10  15888  ramz  15923  ramub1  15926  firest  16287  mremre  16458  isacs2  16507  iscatd2  16535  sscfn1  16670  sscfn2  16671  gsumval2a  17472  symggen  18082  cyggex2  18490  gsumval3  18500  gsumzres  18502  gsumzcl2  18503  gsumzf1o  18505  gsumzaddlem  18513  gsumconst  18526  gsumzmhm  18529  gsumzoppg  18536  gsum2d2  18565  pgpfac1lem5  18670  ablfaclem3  18678  lss0cl  19141  lspsnat  19339  cnsubrg  20000  gsumfsum  20007  obslbs  20268  lmiclbs  20370  lmisfree  20375  mdetdiaglem  20598  mdet0  20606  eltg3  20960  tgtop  20971  tgidm  20978  ppttop  21005  toponmre  21091  tgrest  21157  neitr  21178  tgcn  21250  cmpsublem  21396  cmpsub  21397  iunconnlem  21424  unconn  21426  1stcfb  21442  2ndcctbss  21452  2ndcdisj  21453  1stcelcls  21458  1stccnp  21459  locfincmp  21523  comppfsc  21529  1stckgen  21551  ptuni2  21573  ptbasfi  21578  ptpjopn  21609  ptclsg  21612  ptcnp  21619  prdstopn  21625  txindis  21631  txtube  21637  txcmplem1  21638  txcmplem2  21639  xkococnlem  21656  txconn  21686  trfbas2  21840  filtop  21852  filconn  21880  filssufilg  21908  fmfnfm  21955  ufldom  21959  hauspwpwf1  21984  alexsubALTlem3  22046  alexsubALT  22048  ptcmplem2  22050  tmdgsum2  22093  tgptsmscld  22147  ustfilxp  22209  xbln0  22412  opnreen  22827  metdsre  22849  cnheibor  22947  phtpc01  22988  cfilfcls  23264  cmetcaulem  23278  iscmet3  23283  ovolctb  23450  ovoliunlem3  23464  ovoliunnul  23467  ovolicc2lem5  23481  ovolicc2  23482  dyadmbl  23560  vitali  23573  itg11  23649  bddmulibl  23796  perfdvf  23858  dvcnp2  23874  dvlip  23947  dvne0  23965  fta1g  24118  fta1  24254  ulmcau  24340  pserulm  24367  wilthlem2  24986  dchrvmasumif  25383  rpvmasum2  25392  dchrisum0re  25393  dchrisum0lem3  25399  dchrisum0  25400  dchrmusum  25404  dchrvmasum  25405  axcontlem10  26044  usgr1v0e  26409  wlkiswwlks  26977  wlkiswwlkupgr  26979  wlklnwwlkn  26985  wlklnwwlknupgr  26987  umgrwwlks2on  27070  elwwlks2  27080  elwspths2spth  27081  clwlkclwwlklem3  27116  clwlkclwwlkfo  27124  clwlksfoclwwlkOLD  27209  frgr3vlem2  27420  spansncvi  28812  reff  30207  locfinreflem  30208  cmpcref  30218  fmcncfil  30278  volmeas  30595  omssubadd  30663  bnj849  31294  derangenlem  31452  cvmsss2  31555  cvmopnlem  31559  cvmfolem  31560  cvmliftmolem2  31563  cvmliftlem15  31579  cvmlift2lem10  31593  cvmlift3lem8  31607  fundmpss  31963  frpomin  32036  frmin  32040  frrlem11  32090  nocvxmin  32192  fnessref  32650  refssfne  32651  neibastop2lem  32653  neibastop2  32654  fnemeet2  32660  fnejoin2  32662  tailfb  32670  knoppcnlem9  32789  wl-ax13lem1  33592  wl-sbcom2d  33649  matunitlindflem2  33711  poimirlem25  33739  poimirlem27  33741  heicant  33749  itg2addnclem  33766  sdclem1  33844  fdc  33846  istotbnd3  33875  sstotbnd2  33878  prdsbnd2  33899  heibor1lem  33913  heiborlem1  33915  heiborlem10  33924  heibor  33925  riscer  34092  divrngidl  34132  iss2  34427  prtlem17  34657  ax12eq  34722  ax12el  34723  ax12inda  34729  ax12v2-o  34730  osumcllem8N  35744  pexmidlem5N  35755  mapdrvallem2  37428  clcnvlem  38424  onfrALT  39258  chordthmALT  39660  snelmap  39745  ssnnf1octb  39873  choicefi  39883  mapss2  39888  difmap  39890  axccdom  39907  infxrlesupxr  40153  inficc  40256  fsumnncl  40298  stoweidlem43  40755  stoweidlem48  40760  stoweidlem57  40769  stoweidlem60  40772  qndenserrnopn  41013  issalnnd  41058  subsaliuncl  41071  sge0cl  41093  nnfoctbdj  41168  ismeannd  41179  caragenunicl  41236  isomennd  41243  ovn0lem  41277  ovnsubaddlem2  41283  hspdifhsp  41328  hspmbllem3  41340  smflimlem6  41482  smfpimbor1lem1  41503  smfpimcc  41512  smfsuplem2  41516  rlimdmafv  41755  mgmpropd  42277  c0snmgmhm  42416
  Copyright terms: Public domain W3C validator