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

Theorem rexlimiv 2949
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 2824 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 r19.23v 2943 . 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 1767   A.wral 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  rexlimiva  2951  rexlimivw  2952  rexlimdv  2953  rexlimivv  2960  r19.36av  3009  r19.44av  3018  r19.45av  3019  rexn0  3930  uniss2  4278  disjiun  4437  elres  5307  ssimaex  5930  ordzsl  6658  onzsl  6659  tfrlem5  7046  tfrlem8  7050  nneob  7298  ecoptocl  7398  mapsn  7457  elixpsn  7505  ixpsnf1o  7506  php  7698  php3  7700  ssfi  7737  findcard  7755  findcard2  7756  ordunifi  7766  fiint  7793  en3lp  8029  inf0  8034  inf3lemd  8040  inf3lem6  8046  noinfep  8072  cantnfvalf  8080  trcl  8155  bndrank  8255  rankc2  8285  tcrank  8298  ficardom  8338  ac10ct  8411  isinfcard  8469  alephfp  8485  dfac5lem4  8503  dfac2  8507  ackbij2  8619  fin23lem16  8711  fin23lem29  8717  fin17  8770  fin1a2lem6  8781  itunitc  8797  hsmexlem9  8801  axdc3lem2  8827  axdc3lem4  8829  axcclem  8833  zorn2lem7  8878  wunr1om  9093  tskr1om  9141  grothomex  9203  prnmadd  9371  ltaprlem  9418  mulgt0sr  9478  0re  9592  0cnALT  9805  renegcli  9876  infmrcl  10518  peano2nn  10544  bndndx  10790  uzn0  11093  ublbneg  11162  om2uzrani  12027  uzrdgfni  12033  exprelprel  12490  rexanuz2  13141  caurcvg  13458  caucvg  13460  infcvgaux1i  13627  vdwlem6  14359  efgrelexlemb  16564  cygth  18377  iscldtop  19362  opnneiid  19393  pnfnei  19487  mnfnei  19488  discmp  19664  cmpsublem  19665  cmpfi  19674  bwthOLD  19677  2ndcredom  19717  2ndc1stc  19718  2ndcdisj  19723  kgenidm  19783  methaus  20758  xrtgioo  21046  caun0  21455  ovolmge0  21623  itg2lcl  21869  aannenlem2  22459  aannenlem3  22460  aaliou2  22470  leibpilem1  22999  2sqlem2  23367  ostth  23552  eupatrl  24644  3cyclfrgrarn1  24688  3cyclfrgrarn  24689  zerdivemp1  25112  rngoridfz  25113  h1de2ctlem  26149  h1de2ci  26150  spansni  26151  spanunsni  26173  riesz3i  26657  adjbd1o  26680  rnbra  26702  pjnmopi  26743  dfpjop  26777  atom1d  26948  cvexchlem  26963  cdj1i  27028  cdj3lem1  27029  hasheuni  27731  afsval  28191  cvmlift2lem12  28399  ghomgrpilem2  28501  rtrclreclem.trans  28544  rtrclind  28547  untint  28559  dfon2lem3  28794  dfon2lem7  28798  dfrdg2  28805  trpred0  28896  nodmon  28987  sltval2  28993  bdayfo  29012  nofulllem5  29043  finminlem  29713  fneint  29749  zerdivemp1x  29961  ismrc  30237  eldiophb  30294  eldioph4b  30349  dfacbasgrp  30661  islptre  31161  dochsnnz  36247
  Copyright terms: Public domain W3C validator