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

Theorem rexlimiva 3010
 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 449 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 3009 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  rexraleqim  3299  issn  4303  unon  6923  tfrlem16  7376  oawordeulem  7521  nneob  7619  ominf  8057  unfilem1  8109  pwfi  8144  fival  8201  elfi2  8203  fi0  8209  fiin  8211  finnum  8657  dif1card  8716  fseqenlem2  8731  dfac8alem  8735  alephfp  8814  cflim2  8968  isfin1-3  9091  fin67  9100  isfin7-2  9101  axdc3lem  9155  axdc3lem2  9156  iunfo  9240  iundom2g  9241  winainflem  9394  rankcf  9478  map2psrpr  9810  supsrlem  9811  1re  9918  00id  10090  addid1  10095  om2uzrani  12613  uzrdgfni  12619  wrdf  13165  rexanuz  13933  r19.2uz  13939  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  0dvds  14840  even2n  14904  m1expe  14929  m1exp1  14931  modprm0  15348  cshwsidrepsw  15638  dfgrp2  17270  psgndiflemA  19766  ppttop  20621  epttop  20623  neips  20727  lmmo  20994  2ndctop  21060  2ndcsep  21072  fbncp  21453  fgcl  21492  filuni  21499  tgioo  22407  zcld  22424  elovolm  23050  nulmbl2  23111  ellimc3  23449  limcflf  23451  pilem3  24011  perfect  24756  2vmadivsum  25030  selberg3lem2  25047  selberg4  25050  pntrsumbnd2  25056  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntpbnd  25077  pnt3  25101  axcontlem12  25655  axcont  25656  eleclclwwlkn  26360  frgrareggt1  26643  norm1exi  27491  nmcexi  28269  lnconi  28276  pjssdif1i  28418  stri  28500  hstri  28508  stcltrthi  28521  shatomici  28601  dispcmp  29254  isrnmeas  29590  dya2iocucvr  29673  sxbrsigalem1  29674  eulerpartlemt  29760  bnj1398  30356  bnj1498  30383  mthmblem  30731  trpredlem1  30971  elno  31043  noreson  31057  lindsdom  32573  mblfinlem3  32618  ismblfin  32620  volsupnfl  32624  itg2addnclem  32631  itg2addnc  32634  cover2  32678  prtlem16  33172  rexzrexnn0  36386  isnumbasgrplem2  36693  dgraalem  36734  rp-isfinite5  36882  islptre  38686  stirlinglem13  38979  stirlinglem14  38980  stirling  38982  etransc  39176  ovolval4lem2  39540  prmdvdsfmtnof  40036  prmdvdsfmtnof1  40037  perfectALTV  40166  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  eleclclwwlksn  41260  uhgr3cyclex  41349  av-frgrareggt1  41547  2zlidl  41724  2zrngamgm  41729  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  lincsumcl  42014  lincscmcl  42015  ellcoellss  42018
 Copyright terms: Public domain W3C validator