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

Theorem rexlimiv 2623
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 2622 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  rexlimiva  2624  rexlimivw  2625  rexlimivv  2634  r19.36av  2650  r19.44av  2658  r19.45av  2659  rexn0  3462  uniss2  3756  disjiun  3910  ordzsl  4527  onzsl  4528  elres  4897  ssimaex  5436  tfrlem8  6286  nneob  6536  ecoptocl  6634  mapsn  6695  elixpsn  6741  ixpsnf1o  6742  php  6930  php3  6932  ssfi  6968  findcard  6982  findcard2  6983  ordunifi  6992  fiint  7018  inf0  7206  inf3lemd  7212  inf3lem6  7218  noinfep  7244  cantnfvalf  7250  trcl  7294  en3lp  7302  bndrank  7397  rankc2  7427  tcrank  7438  ficardom  7478  ac10ct  7545  isinfcard  7603  alephfp  7619  dfac5lem4  7637  dfac2  7641  ackbij2  7753  fin23lem16  7845  fin23lem29  7851  fin17  7904  fin1a2lem6  7915  itunitc  7931  hsmexlem9  7935  axdc3lem2  7961  axdc3lem4  7963  axcclem  7967  zorn2lem7  8013  wunr1om  8221  tskr1om  8269  grothomex  8331  prnmadd  8501  ltaprlem  8548  mulgt0sr  8607  0re  8718  0cnALT  8921  renegcli  8988  infmrcl  9613  peano2nn  9638  bndndx  9843  uzn0  10122  ublbneg  10181  om2uzrani  10893  uzrdgfni  10899  rexanuz2  11710  caurcvg  12026  caucvg  12028  infcvgaux1i  12189  vdwlem6  12907  efgrelexlemb  14894  cygth  16357  iscldtop  16664  opnneiid  16695  pnfnei  16782  mnfnei  16783  discmp  16957  cmpsublem  16958  cmpfi  16967  2ndcredom  17008  2ndc1stc  17009  2ndcdisj  17014  kgenidm  17074  methaus  17898  xrtgioo  18144  caun0  18539  ovolmge0  18668  itg2lcl  18914  aannenlem2  19541  aannenlem3  19542  aaliou2  19552  leibpilem1  20068  2sqlem2  20435  ostth  20620  h1de2ctlem  21964  h1de2ci  21965  spansni  21966  spanunsni  21988  riesz3i  22472  adjbd1o  22495  rnbra  22517  pjnmopi  22558  dfpjop  22592  atom1d  22763  cvexchlem  22778  cdj1i  22843  cdj3lem1  22844  cvmlift2lem12  23016  ghomgrpilem2  23164  rtrclreclem.trans  23214  rtrclind  23217  untint  23229  dfon2lem3  23309  dfon2lem7  23313  dfrdg2  23320  trpred0  23407  nodmon  23472  sltval2  23477  axbday  23496  axfelem18  23531  prj1b  24244  prj3  24245  grpodivfo  24540  rltrran  24580  zerdivemp1  24602  rngoridfz  24603  svs2  24653  nsn  24696  intopcoaconlem3  24705  efilcp  24718  cmptdst  24734  prdnei  24739  limptlimpr2lem2  24741  islimrs4  24748  bwt2  24758  cntrset  24768  addcanri  24832  addcanrg  24833  negveud  24834  negveudr  24835  lemindclsbu  25161  gltpntl  25238  iscol3  25260  isibg1a6  25291  lppotos  25310  nbssntrs  25313  pdiveql  25334  finminlem  25397  fneint  25443  zerdivemp1x  25752  ismrc  25942  eldiophb  26002  eldioph4b  26060  dfacbasgrp  26439  dochsnnz  30544
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator