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

Theorem rexlimiv 2918
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 2792 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 r19.23v 2912 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
42, 3mpbi 211 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   A.wral 2782   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788
This theorem is referenced by:  rexlimiva  2920  rexlimivw  2921  rexlimdv  2922  rexlimivv  2929  r19.36v  2983  r19.44v  2992  r19.45v  2993  rexn0  3906  uniss2  4254  disjiun  4417  elres  5160  ssimaex  5946  ordzsl  6686  onzsl  6687  tfrlem8  7110  nneob  7361  ecoptocl  7461  mapsn  7521  elixpsn  7569  ixpsnf1o  7570  php  7762  php3  7764  ssfi  7798  findcard  7816  findcard2  7817  ordunifi  7827  fiint  7854  en3lp  8121  inf0  8126  inf3lemd  8132  inf3lem6  8138  noinfep  8164  cantnfvalf  8169  trcl  8211  bndrank  8311  rankc2  8341  tcrank  8354  ficardom  8394  ac10ct  8463  isinfcard  8521  alephfp  8537  dfac5lem4  8555  dfac2  8559  ackbij2  8671  fin23lem16  8763  fin23lem29  8769  fin17  8822  fin1a2lem6  8833  itunitc  8849  hsmexlem9  8853  axdc3lem2  8879  axdc3lem4  8881  axcclem  8885  zorn2lem7  8930  wunr1om  9143  tskr1om  9191  grothomex  9253  prnmadd  9421  ltaprlem  9468  mulgt0sr  9528  0re  9642  0cnALT  9863  renegcli  9934  infmrclOLD  10593  peano2nn  10621  bndndx  10868  uzn0  11174  ublbneg  11248  om2uzrani  12163  uzrdgfni  12169  exprelprel  12637  rtrclreclem3  13102  rtrclind  13107  rexanuz2  13391  caurcvg  13720  caurcvgOLD  13721  caucvg  13723  infcvgaux1i  13893  vdwlem6  14890  efgrelexlemb  17326  cygth  19064  iscldtop  20033  opnneiid  20064  pnfnei  20158  mnfnei  20159  discmp  20335  cmpsublem  20336  cmpfi  20345  2ndcredom  20387  2ndc1stc  20388  2ndcdisj  20393  kgenidm  20484  methaus  21457  xrtgioo  21726  caun0  22135  ovolmge0  22299  itg2lcl  22553  aannenlem2  23141  aannenlem3  23142  aaliou2  23152  leibpilem1  23722  2sqlem2  24146  ostth  24331  eupatrl  25532  3cyclfrgrarn1  25576  3cyclfrgrarn  25577  zerdivemp1  25998  rngoridfz  25999  h1de2ctlem  27034  h1de2ci  27035  spansni  27036  spanunsni  27058  riesz3i  27541  adjbd1o  27564  rnbra  27586  pjnmopi  27627  dfpjop  27661  atom1d  27832  cvexchlem  27847  cdj1i  27912  cdj3lem1  27913  hasheuni  28736  cvmlift2lem12  29816  mrsubccat  29935  msrid  29962  elmthm  29993  ghomgrpilem2  30083  untint  30118  dfon2lem3  30209  dfon2lem7  30213  dfrdg2  30220  trpred0  30255  nodmon  30315  sltval2  30321  bdayfo  30340  nofulllem5  30371  finminlem  30750  fneint  30780  ptrecube  31634  poimirlem26  31660  poimirlem27  31661  poimirlem29  31663  poimirlem30  31664  zerdivemp1x  31888  dochsnnz  34717  ismrc  35242  eldiophb  35298  eldioph4b  35353  dfacbasgrp  35663
  Copyright terms: Public domain W3C validator