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

Theorem rexlimiv 2868
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 2742 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 r19.23v 2862 . 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 1826   A.wral 2732   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-ral 2737  df-rex 2738
This theorem is referenced by:  rexlimiva  2870  rexlimivw  2871  rexlimdv  2872  rexlimivv  2879  r19.36v  2930  r19.44v  2939  r19.45v  2940  rexn0  3848  uniss2  4195  disjiun  4358  elres  5221  ssimaex  5839  ordzsl  6579  onzsl  6580  tfrlem8  6971  nneob  7219  ecoptocl  7319  mapsn  7379  elixpsn  7427  ixpsnf1o  7428  php  7620  php3  7622  ssfi  7656  findcard  7674  findcard2  7675  ordunifi  7685  fiint  7712  en3lp  7947  inf0  7952  inf3lemd  7958  inf3lem6  7964  noinfep  7990  cantnfvalf  7997  trcl  8072  bndrank  8172  rankc2  8202  tcrank  8215  ficardom  8255  ac10ct  8328  isinfcard  8386  alephfp  8402  dfac5lem4  8420  dfac2  8424  ackbij2  8536  fin23lem16  8628  fin23lem29  8634  fin17  8687  fin1a2lem6  8698  itunitc  8714  hsmexlem9  8718  axdc3lem2  8744  axdc3lem4  8746  axcclem  8750  zorn2lem7  8795  wunr1om  9008  tskr1om  9056  grothomex  9118  prnmadd  9286  ltaprlem  9333  mulgt0sr  9393  0re  9507  0cnALT  9722  renegcli  9793  infmrcl  10438  peano2nn  10464  bndndx  10711  uzn0  11016  ublbneg  11085  om2uzrani  11966  uzrdgfni  11972  exprelprel  12432  rtrclreclem3  12895  rtrclind  12900  rexanuz2  13184  caurcvg  13501  caucvg  13503  infcvgaux1i  13670  vdwlem6  14506  efgrelexlemb  16885  cygth  18701  iscldtop  19682  opnneiid  19713  pnfnei  19807  mnfnei  19808  discmp  19984  cmpsublem  19985  cmpfi  19994  2ndcredom  20036  2ndc1stc  20037  2ndcdisj  20042  kgenidm  20133  methaus  21108  xrtgioo  21396  caun0  21805  ovolmge0  21973  itg2lcl  22219  aannenlem2  22810  aannenlem3  22811  aaliou2  22821  leibpilem1  23387  2sqlem2  23756  ostth  23941  eupatrl  25089  3cyclfrgrarn1  25133  3cyclfrgrarn  25134  zerdivemp1  25553  rngoridfz  25554  h1de2ctlem  26590  h1de2ci  26591  spansni  26592  spanunsni  26614  riesz3i  27097  adjbd1o  27120  rnbra  27142  pjnmopi  27183  dfpjop  27217  atom1d  27388  cvexchlem  27403  cdj1i  27468  cdj3lem1  27469  hasheuni  28233  cvmlift2lem12  28948  mrsubccat  29067  msrid  29094  elmthm  29125  ghomgrpilem2  29215  untint  29250  dfon2lem3  29382  dfon2lem7  29386  dfrdg2  29393  trpred0  29484  nodmon  29575  sltval2  29581  bdayfo  29600  nofulllem5  29631  finminlem  30302  fneint  30332  zerdivemp1x  30524  ismrc  30799  eldiophb  30855  eldioph4b  30910  dfacbasgrp  31225  dochsnnz  37590
  Copyright terms: Public domain W3C validator