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

Theorem rexlimiv 2662
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 1606 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2661 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  rexlimiva  2663  rexlimivw  2664  rexlimivv  2673  r19.36av  2689  r19.44av  2697  r19.45av  2698  rexn0  3557  uniss2  3859  disjiun  4014  ordzsl  4635  onzsl  4636  elres  4989  ssimaex  5545  tfrlem8  6395  nneob  6645  ecoptocl  6743  mapsn  6804  elixpsn  6850  ixpsnf1o  6851  php  7040  php3  7042  ssfi  7078  findcard  7092  findcard2  7093  ordunifi  7102  fiint  7128  inf0  7317  inf3lemd  7323  inf3lem6  7329  noinfep  7355  cantnfvalf  7361  trcl  7405  en3lp  7413  bndrank  7508  rankc2  7538  tcrank  7549  ficardom  7589  ac10ct  7656  isinfcard  7714  alephfp  7730  dfac5lem4  7748  dfac2  7752  ackbij2  7864  fin23lem16  7956  fin23lem29  7962  fin17  8015  fin1a2lem6  8026  itunitc  8042  hsmexlem9  8046  axdc3lem2  8072  axdc3lem4  8074  axcclem  8078  zorn2lem7  8124  wunr1om  8336  tskr1om  8384  grothomex  8446  prnmadd  8616  ltaprlem  8663  mulgt0sr  8722  0re  8833  0cnALT  9036  renegcli  9103  infmrcl  9728  peano2nn  9753  bndndx  9959  uzn0  10238  ublbneg  10297  om2uzrani  11009  uzrdgfni  11015  rexanuz2  11827  caurcvg  12143  caucvg  12145  infcvgaux1i  12309  vdwlem6  13027  efgrelexlemb  15053  cygth  16519  iscldtop  16826  opnneiid  16857  pnfnei  16944  mnfnei  16945  discmp  17119  cmpsublem  17120  cmpfi  17129  2ndcredom  17170  2ndc1stc  17171  2ndcdisj  17176  kgenidm  17236  methaus  18060  xrtgioo  18306  caun0  18701  ovolmge0  18830  itg2lcl  19076  aannenlem2  19703  aannenlem3  19704  aaliou2  19714  leibpilem1  20230  2sqlem2  20597  ostth  20782  h1de2ctlem  22126  h1de2ci  22127  spansni  22128  spanunsni  22150  riesz3i  22634  adjbd1o  22657  rnbra  22679  pjnmopi  22720  dfpjop  22754  atom1d  22925  cvexchlem  22940  cdj1i  23005  cdj3lem1  23006  cvmlift2lem12  23249  ghomgrpilem2  23397  rtrclreclem.trans  23447  rtrclind  23450  untint  23462  dfon2lem3  23542  dfon2lem7  23546  dfrdg2  23553  trpred0  23640  nodmon  23705  sltval2  23710  axbday  23729  axfelem18  23764  prj1b  24477  prj3  24478  grpodivfo  24773  rltrran  24813  zerdivemp1  24835  rngoridfz  24836  svs2  24886  nsn  24929  intopcoaconlem3  24938  efilcp  24951  cmptdst  24967  prdnei  24972  limptlimpr2lem2  24974  islimrs4  24981  bwt2  24991  cntrset  25001  addcanri  25065  addcanrg  25066  negveud  25067  negveudr  25068  lemindclsbu  25394  gltpntl  25471  iscol3  25493  isibg1a6  25524  lppotos  25543  nbssntrs  25546  pdiveql  25567  finminlem  25630  fneint  25676  zerdivemp1x  25985  ismrc  26175  eldiophb  26235  eldioph4b  26293  dfacbasgrp  26672  stirling  27237  dochsnnz  30907
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator