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

Theorem rexlimiv 2816
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 1629 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2815 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  rexlimiva  2817  rexlimivw  2818  rexlimivv  2827  r19.36av  2848  r19.44av  2856  r19.45av  2857  rexn0  3722  uniss2  4038  disjiun  4194  ordzsl  4817  onzsl  4818  elres  5173  ssimaex  5780  tfrlem8  6637  nneob  6887  ecoptocl  6986  mapsn  7047  elixpsn  7093  ixpsnf1o  7094  php  7283  php3  7285  ssfi  7321  findcard  7339  findcard2  7340  ordunifi  7349  fiint  7375  inf0  7568  inf3lemd  7574  inf3lem6  7580  noinfep  7606  cantnfvalf  7612  trcl  7656  en3lp  7664  bndrank  7759  rankc2  7789  tcrank  7800  ficardom  7840  ac10ct  7907  isinfcard  7965  alephfp  7981  dfac5lem4  7999  dfac2  8003  ackbij2  8115  fin23lem16  8207  fin23lem29  8213  fin17  8266  fin1a2lem6  8277  itunitc  8293  hsmexlem9  8297  axdc3lem2  8323  axdc3lem4  8325  axcclem  8329  zorn2lem7  8374  wunr1om  8586  tskr1om  8634  grothomex  8696  prnmadd  8866  ltaprlem  8913  mulgt0sr  8972  0re  9083  0cnALT  9287  renegcli  9354  infmrcl  9979  peano2nn  10004  bndndx  10212  uzn0  10493  ublbneg  10552  om2uzrani  11284  uzrdgfni  11290  rexanuz2  12145  caurcvg  12462  caucvg  12464  infcvgaux1i  12628  vdwlem6  13346  efgrelexlemb  15374  cygth  16844  iscldtop  17151  opnneiid  17182  pnfnei  17276  mnfnei  17277  discmp  17453  cmpsublem  17454  cmpfi  17463  bwth  17465  2ndcredom  17505  2ndc1stc  17506  2ndcdisj  17511  kgenidm  17571  methaus  18542  xrtgioo  18829  caun0  19226  ovolmge0  19365  itg2lcl  19611  aannenlem2  20238  aannenlem3  20239  aaliou2  20249  leibpilem1  20772  2sqlem2  21140  ostth  21325  eupatrl  21682  zerdivemp1  22014  rngoridfz  22015  h1de2ctlem  23049  h1de2ci  23050  spansni  23051  spanunsni  23073  riesz3i  23557  adjbd1o  23580  rnbra  23602  pjnmopi  23643  dfpjop  23677  atom1d  23848  cvexchlem  23863  cdj1i  23928  cdj3lem1  23929  hasheuni  24467  cvmlift2lem12  24993  ghomgrpilem2  25089  rtrclreclem.trans  25138  rtrclind  25141  untint  25153  dfon2lem3  25404  dfon2lem7  25408  dfrdg2  25415  trpred0  25506  nodmon  25597  sltval2  25603  bdayfo  25622  nofulllem5  25653  finminlem  26312  fneint  26348  zerdivemp1x  26562  ismrc  26746  eldiophb  26806  eldioph4b  26863  dfacbasgrp  27241  3cyclfrgrarn1  28339  3cyclfrgrarn  28340  dochsnnz  32185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator