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

Theorem rexlimiv 2939
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 1674 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2938 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   E.wrex 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2803  df-rex 2804
This theorem is referenced by:  rexlimiva  2940  rexlimivw  2941  rexlimivv  2950  r19.36av  2972  r19.44av  2981  r19.45av  2982  rexn0  3889  uniss2  4231  disjiun  4389  elres  5252  ssimaex  5864  ordzsl  6565  onzsl  6566  tfrlem5  6948  tfrlem8  6952  nneob  7200  ecoptocl  7299  mapsn  7363  elixpsn  7411  ixpsnf1o  7412  php  7604  php3  7606  ssfi  7643  findcard  7661  findcard2  7662  ordunifi  7672  fiint  7698  en3lp  7932  inf0  7937  inf3lemd  7943  inf3lem6  7949  noinfep  7975  cantnfvalf  7983  trcl  8058  bndrank  8158  rankc2  8188  tcrank  8201  ficardom  8241  ac10ct  8314  isinfcard  8372  alephfp  8388  dfac5lem4  8406  dfac2  8410  ackbij2  8522  fin23lem16  8614  fin23lem29  8620  fin17  8673  fin1a2lem6  8684  itunitc  8700  hsmexlem9  8704  axdc3lem2  8730  axdc3lem4  8732  axcclem  8736  zorn2lem7  8781  wunr1om  8996  tskr1om  9044  grothomex  9106  prnmadd  9276  ltaprlem  9323  mulgt0sr  9382  0re  9496  0cnALT  9709  renegcli  9780  infmrcl  10419  peano2nn  10444  bndndx  10688  uzn0  10986  ublbneg  11049  om2uzrani  11891  uzrdgfni  11897  rexanuz2  12954  caurcvg  13271  caucvg  13273  infcvgaux1i  13436  vdwlem6  14164  efgrelexlemb  16367  cygth  18128  iscldtop  18830  opnneiid  18861  pnfnei  18955  mnfnei  18956  discmp  19132  cmpsublem  19133  cmpfi  19142  bwthOLD  19145  2ndcredom  19185  2ndc1stc  19186  2ndcdisj  19191  kgenidm  19251  methaus  20226  xrtgioo  20514  caun0  20923  ovolmge0  21091  itg2lcl  21337  aannenlem2  21927  aannenlem3  21928  aaliou2  21938  leibpilem1  22467  2sqlem2  22835  ostth  23020  eupatrl  23740  zerdivemp1  24072  rngoridfz  24073  h1de2ctlem  25109  h1de2ci  25110  spansni  25111  spanunsni  25133  riesz3i  25617  adjbd1o  25640  rnbra  25662  pjnmopi  25703  dfpjop  25737  atom1d  25908  cvexchlem  25923  cdj1i  25988  cdj3lem1  25989  hasheuni  26678  afsval  27138  cvmlift2lem12  27346  ghomgrpilem2  27448  rtrclreclem.trans  27491  rtrclind  27494  untint  27506  dfon2lem3  27741  dfon2lem7  27745  dfrdg2  27752  trpred0  27843  nodmon  27934  sltval2  27940  bdayfo  27959  nofulllem5  27990  finminlem  28660  fneint  28696  zerdivemp1x  28908  ismrc  29184  eldiophb  29242  eldioph4b  29297  dfacbasgrp  29611  exprelprel  30376  3cyclfrgrarn1  30751  3cyclfrgrarn  30752  dochsnnz  35418
  Copyright terms: Public domain W3C validator