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

Theorem rexlimiv 2661
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 1605 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2660 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rexlimiva  2662  rexlimivw  2663  rexlimivv  2672  r19.36av  2688  r19.44av  2696  r19.45av  2697  rexn0  3556  uniss2  3858  disjiun  4013  ordzsl  4636  onzsl  4637  elres  4990  ssimaex  5584  tfrlem8  6400  nneob  6650  ecoptocl  6748  mapsn  6809  elixpsn  6855  ixpsnf1o  6856  php  7045  php3  7047  ssfi  7083  findcard  7097  findcard2  7098  ordunifi  7107  fiint  7133  inf0  7322  inf3lemd  7328  inf3lem6  7334  noinfep  7360  cantnfvalf  7366  trcl  7410  en3lp  7418  bndrank  7513  rankc2  7543  tcrank  7554  ficardom  7594  ac10ct  7661  isinfcard  7719  alephfp  7735  dfac5lem4  7753  dfac2  7757  ackbij2  7869  fin23lem16  7961  fin23lem29  7967  fin17  8020  fin1a2lem6  8031  itunitc  8047  hsmexlem9  8051  axdc3lem2  8077  axdc3lem4  8079  axcclem  8083  zorn2lem7  8129  wunr1om  8341  tskr1om  8389  grothomex  8451  prnmadd  8621  ltaprlem  8668  mulgt0sr  8727  0re  8838  0cnALT  9041  renegcli  9108  infmrcl  9733  peano2nn  9758  bndndx  9964  uzn0  10243  ublbneg  10302  om2uzrani  11015  uzrdgfni  11021  rexanuz2  11833  caurcvg  12149  caucvg  12151  infcvgaux1i  12315  vdwlem6  13033  efgrelexlemb  15059  cygth  16525  iscldtop  16832  opnneiid  16863  pnfnei  16950  mnfnei  16951  discmp  17125  cmpsublem  17126  cmpfi  17135  2ndcredom  17176  2ndc1stc  17177  2ndcdisj  17182  kgenidm  17242  methaus  18066  xrtgioo  18312  caun0  18707  ovolmge0  18836  itg2lcl  19082  aannenlem2  19709  aannenlem3  19710  aaliou2  19720  leibpilem1  20236  2sqlem2  20603  ostth  20788  h1de2ctlem  22134  h1de2ci  22135  spansni  22136  spanunsni  22158  riesz3i  22642  adjbd1o  22665  rnbra  22687  pjnmopi  22728  dfpjop  22762  atom1d  22933  cvexchlem  22948  cdj1i  23013  cdj3lem1  23014  hasheuni  23453  isrnmeas  23531  cvmlift2lem12  23845  ghomgrpilem2  23993  rtrclreclem.trans  24043  rtrclind  24046  untint  24058  ceqsrexv2  24078  dfon2lem3  24141  dfon2lem7  24145  dfrdg2  24152  trpred0  24239  nodmon  24304  sltval2  24310  bdayfo  24329  nofulllem5  24360  prj1b  25079  prj3  25080  grpodivfo  25374  rltrran  25414  zerdivemp1  25436  rngoridfz  25437  svs2  25487  nsn  25530  intopcoaconlem3  25539  efilcp  25552  cmptdst  25568  prdnei  25573  limptlimpr2lem2  25575  islimrs4  25582  bwt2  25592  cntrset  25602  addcanri  25666  addcanrg  25667  negveud  25668  negveudr  25669  lemindclsbu  25995  gltpntl  26072  iscol3  26094  isibg1a6  26125  lppotos  26144  nbssntrs  26147  pdiveql  26168  finminlem  26231  fneint  26277  zerdivemp1x  26586  ismrc  26776  eldiophb  26836  eldioph4b  26894  dfacbasgrp  27273  stirling  27838  usgranloop  28124  dochsnnz  31640
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator