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

Theorem rexlimiv 2634
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 2633 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  rexlimiva  2635  rexlimivw  2636  rexlimivv  2645  r19.36av  2661  r19.44av  2669  r19.45av  2670  rexn0  3517  uniss2  3818  disjiun  3973  ordzsl  4594  onzsl  4595  elres  4964  ssimaex  5504  tfrlem8  6354  nneob  6604  ecoptocl  6702  mapsn  6763  elixpsn  6809  ixpsnf1o  6810  php  6999  php3  7001  ssfi  7037  findcard  7051  findcard2  7052  ordunifi  7061  fiint  7087  inf0  7276  inf3lemd  7282  inf3lem6  7288  noinfep  7314  cantnfvalf  7320  trcl  7364  en3lp  7372  bndrank  7467  rankc2  7497  tcrank  7508  ficardom  7548  ac10ct  7615  isinfcard  7673  alephfp  7689  dfac5lem4  7707  dfac2  7711  ackbij2  7823  fin23lem16  7915  fin23lem29  7921  fin17  7974  fin1a2lem6  7985  itunitc  8001  hsmexlem9  8005  axdc3lem2  8031  axdc3lem4  8033  axcclem  8037  zorn2lem7  8083  wunr1om  8295  tskr1om  8343  grothomex  8405  prnmadd  8575  ltaprlem  8622  mulgt0sr  8681  0re  8792  0cnALT  8995  renegcli  9062  infmrcl  9687  peano2nn  9712  bndndx  9917  uzn0  10196  ublbneg  10255  om2uzrani  10967  uzrdgfni  10973  rexanuz2  11784  caurcvg  12100  caucvg  12102  infcvgaux1i  12263  vdwlem6  12981  efgrelexlemb  15007  cygth  16473  iscldtop  16780  opnneiid  16811  pnfnei  16898  mnfnei  16899  discmp  17073  cmpsublem  17074  cmpfi  17083  2ndcredom  17124  2ndc1stc  17125  2ndcdisj  17130  kgenidm  17190  methaus  18014  xrtgioo  18260  caun0  18655  ovolmge0  18784  itg2lcl  19030  aannenlem2  19657  aannenlem3  19658  aaliou2  19668  leibpilem1  20184  2sqlem2  20551  ostth  20736  h1de2ctlem  22080  h1de2ci  22081  spansni  22082  spanunsni  22104  riesz3i  22588  adjbd1o  22611  rnbra  22633  pjnmopi  22674  dfpjop  22708  atom1d  22879  cvexchlem  22894  cdj1i  22959  cdj3lem1  22960  cvmlift2lem12  23203  ghomgrpilem2  23351  rtrclreclem.trans  23401  rtrclind  23404  untint  23416  dfon2lem3  23496  dfon2lem7  23500  dfrdg2  23507  trpred0  23594  nodmon  23659  sltval2  23664  axbday  23683  axfelem18  23718  prj1b  24431  prj3  24432  grpodivfo  24727  rltrran  24767  zerdivemp1  24789  rngoridfz  24790  svs2  24840  nsn  24883  intopcoaconlem3  24892  efilcp  24905  cmptdst  24921  prdnei  24926  limptlimpr2lem2  24928  islimrs4  24935  bwt2  24945  cntrset  24955  addcanri  25019  addcanrg  25020  negveud  25021  negveudr  25022  lemindclsbu  25348  gltpntl  25425  iscol3  25447  isibg1a6  25478  lppotos  25497  nbssntrs  25500  pdiveql  25521  finminlem  25584  fneint  25630  zerdivemp1x  25939  ismrc  26129  eldiophb  26189  eldioph4b  26247  dfacbasgrp  26626  dochsnnz  30791
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 2521  df-rex 2522
  Copyright terms: Public domain W3C validator