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

Theorem rexlimiva 3273
 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 416 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 3272 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2115  ∃wrex 3133 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3137  df-rex 3138 This theorem is referenced by:  rexraleqim  3625  rexopabb  5396  unon  7529  tfrlem16  8012  oawordeulem  8163  nneob  8262  ominf  8714  unfilem1  8766  pwfi  8803  fival  8860  elfi2  8862  fi0  8868  fiin  8870  djuss  9333  djuun  9339  updjud  9347  finnum  9361  dif1card  9421  fseqenlem2  9436  dfac8alem  9440  alephfp  9519  cflim2  9670  isfin1-3  9793  fin67  9802  isfin7-2  9803  axdc3lem  9857  axdc3lem2  9858  iunfo  9946  iundom2g  9947  winainflem  10100  rankcf  10184  map2psrpr  10517  supsrlem  10518  1re  10626  0re  10628  00id  10800  addid1  10805  0cnALT  10859  om2uzrani  13313  uzrdgfni  13319  wrdf  13860  rexanuz  14694  r19.2uz  14700  fsum2dlem  15114  fsumcom2  15118  fprod2dlem  15323  fprodcom2  15327  0dvds  15619  even2n  15680  m1expe  15712  m1exp1  15714  modprm0  16129  cshwsidrepsw  16416  smndex1basss  18059  smndex1mgm  18061  smndex1mndlem  18063  dfgrp2  18117  psgndiflemA  20731  ppttop  21601  epttop  21603  neips  21707  lmmo  21974  2ndctop  22041  2ndcsep  22053  fbncp  22433  fgcl  22472  filuni  22479  tgioo  23390  zcld  23407  cphsscph  23844  elovolm  24068  nulmbl2  24129  ellimc3  24471  limcflf  24473  pilem3  25037  perfect  25804  2vmadivsum  26114  selberg3lem2  26131  selberg4  26134  pntrsumbnd2  26140  pntrlog2bndlem3  26152  pntrlog2bndlem4  26153  pntpbnd  26161  pnt3  26185  axcontlem12  26758  axcont  26759  clwwlkn1loopb  27817  eleclclwwlkn  27850  uhgr3cyclex  27956  frgrreggt1  28167  norm1exi  29022  nmcexi  29798  lnconi  29805  pjssdif1i  29947  stri  30029  hstri  30037  stcltrthi  30050  shatomici  30130  qsxpid  30945  dispcmp  31144  isrnmeas  31477  dya2iocucvr  31560  sxbrsigalem1  31561  eulerpartlemt  31647  bnj1398  32324  bnj1498  32351  satfrnmapom  32635  gonar  32660  goalr  32662  satffun  32674  mthmblem  32845  trpredlem1  33084  elno  33171  noreson  33185  nosupbnd1lem5  33230  lindsdom  34951  mblfinlem3  34996  ismblfin  34998  volsupnfl  35002  itg2addnclem  35008  itg2addnc  35011  cover2  35052  prtlem16  36065  rexzrexnn0  39577  isnumbasgrplem2  39880  dgraalem  39921  rp-isfinite5  40057  mnurndlem1  40825  grumnudlem  40829  gruex  40842  islptre  42103  stirlinglem13  42570  stirlinglem14  42571  stirling  42573  etransc  42767  ovolval4lem2  43131  sprsymrelf1lem  43850  sprsymrelfolem2  43852  prmdvdsfmtnof  43945  prmdvdsfmtnof1  43946  perfectALTV  44083  tgoldbach  44177  uspgrsprf  44216  2zlidl  44400  2zrngamgm  44405  ply1mulgsumlem1  44635  ply1mulgsumlem2  44636  lincsumcl  44681  lincscmcl  44682  ellcoellss  44685
 Copyright terms: Public domain W3C validator