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

Theorem rexlimiv 2737
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 1619 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2736 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  rexlimiva  2738  rexlimivw  2739  rexlimivv  2748  r19.36av  2764  r19.44av  2772  r19.45av  2773  rexn0  3632  uniss2  3939  disjiun  4094  ordzsl  4718  onzsl  4719  elres  5072  ssimaex  5667  tfrlem8  6487  nneob  6737  ecoptocl  6836  mapsn  6897  elixpsn  6943  ixpsnf1o  6944  php  7133  php3  7135  ssfi  7171  findcard  7187  findcard2  7188  ordunifi  7197  fiint  7223  inf0  7412  inf3lemd  7418  inf3lem6  7424  noinfep  7450  cantnfvalf  7456  trcl  7500  en3lp  7508  bndrank  7603  rankc2  7633  tcrank  7644  ficardom  7684  ac10ct  7751  isinfcard  7809  alephfp  7825  dfac5lem4  7843  dfac2  7847  ackbij2  7959  fin23lem16  8051  fin23lem29  8057  fin17  8110  fin1a2lem6  8121  itunitc  8137  hsmexlem9  8141  axdc3lem2  8167  axdc3lem4  8169  axcclem  8173  zorn2lem7  8219  wunr1om  8431  tskr1om  8479  grothomex  8541  prnmadd  8711  ltaprlem  8758  mulgt0sr  8817  0re  8928  0cnALT  9131  renegcli  9198  infmrcl  9823  peano2nn  9848  bndndx  10056  uzn0  10335  ublbneg  10394  om2uzrani  11107  uzrdgfni  11113  rexanuz2  11929  caurcvg  12246  caucvg  12248  infcvgaux1i  12412  vdwlem6  13130  efgrelexlemb  15158  cygth  16631  iscldtop  16938  opnneiid  16969  pnfnei  17056  mnfnei  17057  discmp  17231  cmpsublem  17232  cmpfi  17241  2ndcredom  17282  2ndc1stc  17283  2ndcdisj  17288  kgenidm  17348  methaus  18168  xrtgioo  18414  caun0  18811  ovolmge0  18940  itg2lcl  19186  aannenlem2  19813  aannenlem3  19814  aaliou2  19824  leibpilem1  20347  2sqlem2  20715  ostth  20900  zerdivemp1  21213  rngoridfz  21214  h1de2ctlem  22248  h1de2ci  22249  spansni  22250  spanunsni  22272  riesz3i  22756  adjbd1o  22779  rnbra  22801  pjnmopi  22842  dfpjop  22876  atom1d  23047  cvexchlem  23062  cdj1i  23127  cdj3lem1  23128  hasheuni  23741  isrnmeas  23820  cvmlift2lem12  24249  ghomgrpilem2  24397  rtrclreclem.trans  24447  rtrclind  24450  untint  24462  ceqsrexv2  24482  dfon2lem3  24699  dfon2lem7  24703  dfrdg2  24710  trpred0  24797  nodmon  24862  sltval2  24868  bdayfo  24887  nofulllem5  24918  finminlem  25555  fneint  25601  zerdivemp1x  25909  ismrc  26099  eldiophb  26159  eldioph4b  26217  dfacbasgrp  26596  stirling  27161  usgranloop  27553  eupatrl  27763  3cyclfrgrarn1  27845  3cyclfrgrarn  27846  dochsnnz  31709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2624  df-rex 2625
  Copyright terms: Public domain W3C validator