MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimiv Structured version   Unicode version

Theorem rexlimiv 2830
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
rexlimiv.1  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimiv  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimiv
StepHypRef Expression
1 nfv 1673 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2829 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  rexlimiva  2831  rexlimivw  2832  rexlimivv  2841  r19.36av  2863  r19.44av  2872  r19.45av  2873  rexn0  3777  uniss2  4119  disjiun  4277  elres  5140  ssimaex  5751  ordzsl  6451  onzsl  6452  tfrlem5  6831  tfrlem8  6835  nneob  7083  ecoptocl  7182  mapsn  7246  elixpsn  7294  ixpsnf1o  7295  php  7487  php3  7489  ssfi  7525  findcard  7543  findcard2  7544  ordunifi  7554  fiint  7580  en3lp  7814  inf0  7819  inf3lemd  7825  inf3lem6  7831  noinfep  7857  cantnfvalf  7865  trcl  7940  bndrank  8040  rankc2  8070  tcrank  8083  ficardom  8123  ac10ct  8196  isinfcard  8254  alephfp  8270  dfac5lem4  8288  dfac2  8292  ackbij2  8404  fin23lem16  8496  fin23lem29  8502  fin17  8555  fin1a2lem6  8566  itunitc  8582  hsmexlem9  8586  axdc3lem2  8612  axdc3lem4  8614  axcclem  8618  zorn2lem7  8663  wunr1om  8878  tskr1om  8926  grothomex  8988  prnmadd  9158  ltaprlem  9205  mulgt0sr  9264  0re  9378  0cnALT  9591  renegcli  9662  infmrcl  10301  peano2nn  10326  bndndx  10570  uzn0  10868  ublbneg  10931  om2uzrani  11767  uzrdgfni  11773  rexanuz2  12829  caurcvg  13146  caucvg  13148  infcvgaux1i  13311  vdwlem6  14039  efgrelexlemb  16238  cygth  17979  iscldtop  18674  opnneiid  18705  pnfnei  18799  mnfnei  18800  discmp  18976  cmpsublem  18977  cmpfi  18986  bwthOLD  18989  2ndcredom  19029  2ndc1stc  19030  2ndcdisj  19035  kgenidm  19095  methaus  20070  xrtgioo  20358  caun0  20767  ovolmge0  20935  itg2lcl  21180  aannenlem2  21770  aannenlem3  21771  aaliou2  21781  leibpilem1  22310  2sqlem2  22678  ostth  22863  eupatrl  23540  zerdivemp1  23872  rngoridfz  23873  h1de2ctlem  24909  h1de2ci  24910  spansni  24911  spanunsni  24933  riesz3i  25417  adjbd1o  25440  rnbra  25462  pjnmopi  25503  dfpjop  25537  atom1d  25708  cvexchlem  25723  cdj1i  25788  cdj3lem1  25789  hasheuni  26486  afsval  26947  cvmlift2lem12  27155  ghomgrpilem2  27256  rtrclreclem.trans  27299  rtrclind  27302  untint  27314  dfon2lem3  27549  dfon2lem7  27553  dfrdg2  27560  trpred0  27651  nodmon  27742  sltval2  27748  bdayfo  27767  nofulllem5  27798  finminlem  28466  fneint  28502  zerdivemp1x  28714  ismrc  28990  eldiophb  29048  eldioph4b  29103  dfacbasgrp  29417  exprelprel  30182  3cyclfrgrarn1  30557  3cyclfrgrarn  30558  dochsnnz  34935
  Copyright terms: Public domain W3C validator