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

Theorem rexlimiva 3024
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
Hypothesis
Ref Expression
rexlimiva.1 ((𝑥𝐴𝜑) → 𝜓)
Assertion
Ref Expression
rexlimiva (∃𝑥𝐴 𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva
StepHypRef Expression
1 rexlimiva.1 . . 3 ((𝑥𝐴𝜑) → 𝜓)
21ex 450 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 3023 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1988  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-ral 2914  df-rex 2915
This theorem is referenced by:  rexraleqim  3323  unon  7016  tfrlem16  7474  oawordeulem  7619  nneob  7717  ominf  8157  unfilem1  8209  pwfi  8246  fival  8303  elfi2  8305  fi0  8311  fiin  8313  finnum  8759  dif1card  8818  fseqenlem2  8833  dfac8alem  8837  alephfp  8916  cflim2  9070  isfin1-3  9193  fin67  9202  isfin7-2  9203  axdc3lem  9257  axdc3lem2  9258  iunfo  9346  iundom2g  9347  winainflem  9500  rankcf  9584  map2psrpr  9916  supsrlem  9917  1re  10024  00id  10196  addid1  10201  om2uzrani  12734  uzrdgfni  12740  wrdf  13293  rexanuz  14066  r19.2uz  14072  fsum2dlem  14482  fsumcom2  14486  fsumcom2OLD  14487  fprod2dlem  14691  fprodcom2  14695  fprodcom2OLD  14696  0dvds  14983  even2n  15047  m1expe  15072  m1exp1  15074  modprm0  15491  cshwsidrepsw  15781  dfgrp2  17428  psgndiflemA  19928  ppttop  20792  epttop  20794  neips  20898  lmmo  21165  2ndctop  21231  2ndcsep  21243  fbncp  21624  fgcl  21663  filuni  21670  tgioo  22580  zcld  22597  elovolm  23224  nulmbl2  23285  ellimc3  23624  limcflf  23626  pilem3  24188  perfect  24937  2vmadivsum  25211  selberg3lem2  25228  selberg4  25231  pntrsumbnd2  25237  pntrlog2bndlem3  25249  pntrlog2bndlem4  25250  pntpbnd  25258  pnt3  25282  axcontlem12  25836  axcont  25837  eleclclwwlksn  26933  uhgr3cyclex  27022  frgrreggt1  27221  norm1exi  28077  nmcexi  28855  lnconi  28862  pjssdif1i  29004  stri  29086  hstri  29094  stcltrthi  29107  shatomici  29187  dispcmp  29900  isrnmeas  30237  dya2iocucvr  30320  sxbrsigalem1  30321  eulerpartlemt  30407  bnj1398  31076  bnj1498  31103  mthmblem  31451  trpredlem1  31701  elno  31773  noreson  31787  nosupbnd1lem5  31832  lindsdom  33374  mblfinlem3  33419  ismblfin  33421  volsupnfl  33425  itg2addnclem  33432  itg2addnc  33435  cover2  33479  prtlem16  33973  rexzrexnn0  37187  isnumbasgrplem2  37493  dgraalem  37534  rp-isfinite5  37682  islptre  39651  stirlinglem13  40066  stirlinglem14  40067  stirling  40069  etransc  40263  ovolval4lem2  40627  prmdvdsfmtnof  41263  prmdvdsfmtnof1  41264  perfectALTV  41397  tgoldbach  41470  tgblthelfgottOLD  41474  tgoldbachOLD  41477  sprsymrelf1lem  41506  sprsymrelfolem2  41508  uspgrsprf  41519  2zlidl  41699  2zrngamgm  41704  ply1mulgsumlem1  41939  ply1mulgsumlem2  41940  lincsumcl  41985  lincscmcl  41986  ellcoellss  41989
  Copyright terms: Public domain W3C validator