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

Theorem rexlimiv 2788
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 1626 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2787 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2671
This theorem is referenced by:  rexlimiva  2789  rexlimivw  2790  rexlimivv  2799  r19.36av  2820  r19.44av  2828  r19.45av  2829  rexn0  3694  uniss2  4010  disjiun  4166  ordzsl  4788  onzsl  4789  elres  5144  ssimaex  5751  tfrlem8  6608  nneob  6858  ecoptocl  6957  mapsn  7018  elixpsn  7064  ixpsnf1o  7065  php  7254  php3  7256  ssfi  7292  findcard  7310  findcard2  7311  ordunifi  7320  fiint  7346  inf0  7536  inf3lemd  7542  inf3lem6  7548  noinfep  7574  cantnfvalf  7580  trcl  7624  en3lp  7632  bndrank  7727  rankc2  7757  tcrank  7768  ficardom  7808  ac10ct  7875  isinfcard  7933  alephfp  7949  dfac5lem4  7967  dfac2  7971  ackbij2  8083  fin23lem16  8175  fin23lem29  8181  fin17  8234  fin1a2lem6  8245  itunitc  8261  hsmexlem9  8265  axdc3lem2  8291  axdc3lem4  8293  axcclem  8297  zorn2lem7  8342  wunr1om  8554  tskr1om  8602  grothomex  8664  prnmadd  8834  ltaprlem  8881  mulgt0sr  8940  0re  9051  0cnALT  9255  renegcli  9322  infmrcl  9947  peano2nn  9972  bndndx  10180  uzn0  10461  ublbneg  10520  om2uzrani  11251  uzrdgfni  11257  rexanuz2  12112  caurcvg  12429  caucvg  12431  infcvgaux1i  12595  vdwlem6  13313  efgrelexlemb  15341  cygth  16811  iscldtop  17118  opnneiid  17149  pnfnei  17242  mnfnei  17243  discmp  17419  cmpsublem  17420  cmpfi  17429  2ndcredom  17470  2ndc1stc  17471  2ndcdisj  17476  kgenidm  17536  methaus  18507  xrtgioo  18794  caun0  19191  ovolmge0  19330  itg2lcl  19576  aannenlem2  20203  aannenlem3  20204  aaliou2  20214  leibpilem1  20737  2sqlem2  21105  ostth  21290  eupatrl  21647  zerdivemp1  21979  rngoridfz  21980  h1de2ctlem  23014  h1de2ci  23015  spansni  23016  spanunsni  23038  riesz3i  23522  adjbd1o  23545  rnbra  23567  pjnmopi  23608  dfpjop  23642  atom1d  23813  cvexchlem  23828  cdj1i  23893  cdj3lem1  23894  hasheuni  24432  cvmlift2lem12  24958  ghomgrpilem2  25054  rtrclreclem.trans  25103  rtrclind  25106  untint  25118  dfon2lem3  25359  dfon2lem7  25363  dfrdg2  25370  trpred0  25457  nodmon  25522  sltval2  25528  bdayfo  25547  nofulllem5  25578  finminlem  26215  fneint  26251  zerdivemp1x  26465  ismrc  26649  eldiophb  26709  eldioph4b  26766  dfacbasgrp  27145  3cyclfrgrarn1  28120  3cyclfrgrarn  28121  dochsnnz  31937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675  df-rex 2676
  Copyright terms: Public domain W3C validator