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

Theorem rexlimiv 2825
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 1672 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2824 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  rexlimiva  2826  rexlimivw  2827  rexlimivv  2836  r19.36av  2858  r19.44av  2867  r19.45av  2868  rexn0  3770  uniss2  4112  disjiun  4270  elres  5133  ssimaex  5744  ordzsl  6445  onzsl  6446  tfrlem5  6825  tfrlem8  6829  nneob  7079  ecoptocl  7178  mapsn  7242  elixpsn  7290  ixpsnf1o  7291  php  7483  php3  7485  ssfi  7521  findcard  7539  findcard2  7540  ordunifi  7550  fiint  7576  en3lp  7810  inf0  7815  inf3lemd  7821  inf3lem6  7827  noinfep  7853  cantnfvalf  7861  trcl  7936  bndrank  8036  rankc2  8066  tcrank  8079  ficardom  8119  ac10ct  8192  isinfcard  8250  alephfp  8266  dfac5lem4  8284  dfac2  8288  ackbij2  8400  fin23lem16  8492  fin23lem29  8498  fin17  8551  fin1a2lem6  8562  itunitc  8578  hsmexlem9  8582  axdc3lem2  8608  axdc3lem4  8610  axcclem  8614  zorn2lem7  8659  wunr1om  8874  tskr1om  8922  grothomex  8984  prnmadd  9154  ltaprlem  9201  mulgt0sr  9260  0re  9374  0cnALT  9587  renegcli  9658  infmrcl  10297  peano2nn  10322  bndndx  10566  uzn0  10864  ublbneg  10927  om2uzrani  11759  uzrdgfni  11765  rexanuz2  12821  caurcvg  13138  caucvg  13140  infcvgaux1i  13302  vdwlem6  14030  efgrelexlemb  16227  cygth  17846  iscldtop  18541  opnneiid  18572  pnfnei  18666  mnfnei  18667  discmp  18843  cmpsublem  18844  cmpfi  18853  bwthOLD  18856  2ndcredom  18896  2ndc1stc  18897  2ndcdisj  18902  kgenidm  18962  methaus  19937  xrtgioo  20225  caun0  20634  ovolmge0  20802  itg2lcl  21047  aannenlem2  21680  aannenlem3  21681  aaliou2  21691  leibpilem1  22220  2sqlem2  22588  ostth  22773  eupatrl  23412  zerdivemp1  23744  rngoridfz  23745  h1de2ctlem  24781  h1de2ci  24782  spansni  24783  spanunsni  24805  riesz3i  25289  adjbd1o  25312  rnbra  25334  pjnmopi  25375  dfpjop  25409  atom1d  25580  cvexchlem  25595  cdj1i  25660  cdj3lem1  25661  hasheuni  26388  afsval  26843  cvmlift2lem12  27051  ghomgrpilem2  27152  rtrclreclem.trans  27195  rtrclind  27198  untint  27210  dfon2lem3  27445  dfon2lem7  27449  dfrdg2  27456  trpred0  27547  nodmon  27638  sltval2  27644  bdayfo  27663  nofulllem5  27694  finminlem  28357  fneint  28393  zerdivemp1x  28605  ismrc  28882  eldiophb  28940  eldioph4b  28995  dfacbasgrp  29309  exprelprel  30075  3cyclfrgrarn1  30450  3cyclfrgrarn  30451  dochsnnz  34668
  Copyright terms: Public domain W3C validator