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

Theorem rexlimiva 3009
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 448 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 3008 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  rexraleqim  3298  unon  6900  tfrlem16  7353  oawordeulem  7498  nneob  7596  ominf  8034  unfilem1  8086  pwfi  8121  fival  8178  elfi2  8180  fi0  8186  fiin  8188  finnum  8634  dif1card  8693  fseqenlem2  8708  dfac8alem  8712  alephfp  8791  cflim2  8945  isfin1-3  9068  fin67  9077  isfin7-2  9078  axdc3lem  9132  axdc3lem2  9133  iunfo  9217  iundom2g  9218  winainflem  9371  rankcf  9455  map2psrpr  9787  supsrlem  9788  1re  9895  00id  10062  addid1  10067  om2uzrani  12568  uzrdgfni  12574  wrdf  13111  rexanuz  13879  r19.2uz  13885  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  0dvds  14786  even2n  14850  m1expe  14875  m1exp1  14877  modprm0  15294  cshwsidrepsw  15584  dfgrp2  17216  psgndiflemA  19711  ppttop  20563  epttop  20565  neips  20669  lmmo  20936  2ndctop  21002  2ndcsep  21014  fbncp  21395  fgcl  21434  filuni  21441  tgioo  22339  zcld  22356  elovolm  22967  nulmbl2  23028  ellimc3  23366  limcflf  23368  pilem3  23928  perfect  24673  2vmadivsum  24947  selberg3lem2  24964  selberg4  24967  pntrsumbnd2  24973  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntpbnd  24994  pnt3  25018  axcontlem12  25573  axcont  25574  eleclclwwlkn  26126  frgrareggt1  26409  norm1exi  27297  nmcexi  28075  lnconi  28082  pjssdif1i  28224  stri  28306  hstri  28314  stcltrthi  28327  shatomici  28407  dispcmp  29060  isrnmeas  29396  dya2iocucvr  29479  sxbrsigalem1  29480  eulerpartlemt  29566  bnj1398  30162  bnj1498  30189  mthmblem  30537  trpredlem1  30777  elno  30849  noreson  30863  lindsdom  32369  mblfinlem3  32414  ismblfin  32416  volsupnfl  32420  itg2addnclem  32427  itg2addnc  32430  cover2  32474  prtlem16  32968  rexzrexnn0  36182  isnumbasgrplem2  36489  dgraalem  36530  rp-isfinite5  36678  islptre  38483  stirlinglem13  38776  stirlinglem14  38777  stirling  38779  etransc  38973  ovolval4lem2  39337  prmdvdsfmtnof  39834  prmdvdsfmtnof1  39835  perfectALTV  39964  tgoldbach  40030  tgblthelfgottOLD  40034  tgoldbachOLD  40037  issn  40115  eleclclwwlksn  41255  uhgr3cyclex  41344  av-frgrareggt1  41542  2zlidl  41719  2zrngamgm  41724  ply1mulgsumlem1  41963  ply1mulgsumlem2  41964  lincsumcl  42009  lincscmcl  42010  ellcoellss  42013
  Copyright terms: Public domain W3C validator