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

Theorem rexlimiv 2929
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
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 rexlimiv.1 . . 3  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
21rgen 2803 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 r19.23v 2923 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
42, 3mpbi 208 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   A.wral 2793   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  rexlimiva  2931  rexlimivw  2932  rexlimdv  2933  rexlimivv  2940  r19.36av  2991  r19.44av  3000  r19.45av  3001  rexn0  3917  uniss2  4267  disjiun  4427  elres  5299  ssimaex  5923  ordzsl  6665  onzsl  6666  tfrlem8  7055  nneob  7303  ecoptocl  7403  mapsn  7462  elixpsn  7510  ixpsnf1o  7511  php  7703  php3  7705  ssfi  7742  findcard  7761  findcard2  7762  ordunifi  7772  fiint  7799  en3lp  8036  inf0  8041  inf3lemd  8047  inf3lem6  8053  noinfep  8079  cantnfvalf  8087  trcl  8162  bndrank  8262  rankc2  8292  tcrank  8305  ficardom  8345  ac10ct  8418  isinfcard  8476  alephfp  8492  dfac5lem4  8510  dfac2  8514  ackbij2  8626  fin23lem16  8718  fin23lem29  8724  fin17  8777  fin1a2lem6  8788  itunitc  8804  hsmexlem9  8808  axdc3lem2  8834  axdc3lem4  8836  axcclem  8840  zorn2lem7  8885  wunr1om  9100  tskr1om  9148  grothomex  9210  prnmadd  9378  ltaprlem  9425  mulgt0sr  9485  0re  9599  0cnALT  9814  renegcli  9885  infmrcl  10528  peano2nn  10554  bndndx  10800  uzn0  11105  ublbneg  11175  om2uzrani  12042  uzrdgfni  12048  exprelprel  12507  rexanuz2  13161  caurcvg  13478  caucvg  13480  infcvgaux1i  13647  vdwlem6  14381  efgrelexlemb  16642  cygth  18483  iscldtop  19469  opnneiid  19500  pnfnei  19594  mnfnei  19595  discmp  19771  cmpsublem  19772  cmpfi  19781  bwthOLD  19784  2ndcredom  19824  2ndc1stc  19825  2ndcdisj  19830  kgenidm  19921  methaus  20896  xrtgioo  21184  caun0  21593  ovolmge0  21761  itg2lcl  22007  aannenlem2  22597  aannenlem3  22598  aaliou2  22608  leibpilem1  23143  2sqlem2  23511  ostth  23696  eupatrl  24840  3cyclfrgrarn1  24884  3cyclfrgrarn  24885  zerdivemp1  25308  rngoridfz  25309  h1de2ctlem  26345  h1de2ci  26346  spansni  26347  spanunsni  26369  riesz3i  26853  adjbd1o  26876  rnbra  26898  pjnmopi  26939  dfpjop  26973  atom1d  27144  cvexchlem  27159  cdj1i  27224  cdj3lem1  27225  hasheuni  27964  cvmlift2lem12  28632  mrsubccat  28751  msrid  28778  elmthm  28809  ghomgrpilem2  28899  rtrclreclem.trans  28942  rtrclind  28945  untint  28957  dfon2lem3  29192  dfon2lem7  29196  dfrdg2  29203  trpred0  29294  nodmon  29385  sltval2  29391  bdayfo  29410  nofulllem5  29441  finminlem  30111  fneint  30141  zerdivemp1x  30333  ismrc  30608  eldiophb  30665  eldioph4b  30720  dfacbasgrp  31032  dochsnnz  36917
  Copyright terms: Public domain W3C validator