Theorem rexlimiv 3027

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

Step	Hyp	Ref	Expression
1		rexlimiv.1	. . 3 |- ( x e. A -> ( ph -> ps ) )
2	1	rgen 2922	. 2 |- A. x e. A ( ph -> ps )
3		r19.23v 3023	. 2 |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )
4	2, 3	mpbi 220	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   e. wcel 1990   A.wral 2912   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexlimiva  3028  rexlimivw  3029  rexlimdv  3030  rexlimivv  3036  clel5  3343  rexn0  4074  issn  4363  uniss2  4470  disjiun  4640  elres  5435  ssimaex  6263  ordzsl  7045  onzsl  7046  tfrlem8  7480  nneob  7732  ecoptocl  7837  mapsn  7899  elixpsn  7947  ixpsnf1o  7948  php  8144  php3  8146  ssfi  8180  findcard  8199  findcard2  8200  ordunifi  8210  fiint  8237  en3lp  8513  inf0  8518  inf3lemd  8524  inf3lem6  8530  noinfep  8557  cantnfvalf  8562  trcl  8604  bndrank  8704  rankc2  8734  tcrank  8747  ficardom  8787  ac10ct  8857  isinfcard  8915  alephfp  8931  dfac5lem4  8949  dfac2  8953  ackbij2  9065  fin23lem16  9157  fin23lem29  9163  fin17  9216  fin1a2lem6  9227  itunitc  9243  hsmexlem9  9247  axdc3lem2  9273  axdc3lem4  9275  axcclem  9279  zorn2lem7  9324  wunr1om  9541  tskr1om  9589  grothomex  9651  prnmadd  9819  ltaprlem  9866  mulgt0sr  9926  0re  10040  0cnALT  10270  renegcli  10342  peano2nn  11032  bndndx  11291  uzn0  11703  ublbneg  11773  om2uzrani  12751  uzrdgfni  12757  exprelprel  13271  rtrclreclem3  13800  rtrclind  13805  rexanuz2  14089  caurcvg  14407  caucvg  14409  infcvgaux1i  14589  vdwlem6  15690  dfgrp2e  17448  efgrelexlemb  18163  cygth  19920  iscldtop  20899  opnneiid  20930  pnfnei  21024  mnfnei  21025  discmp  21201  cmpsublem  21202  cmpfi  21211  2ndcredom  21253  2ndc1stc  21254  2ndcdisj  21259  kgenidm  21350  methaus  22325  xrtgioo  22609  caun0  23079  ovolmge0  23245  itg2lcl  23494  aannenlem2  24084  aannenlem3  24085  aaliou2  24095  leibpilem1  24667  2lgslem1b  25117  2sqlem2  25143  ostth  25328  midwwlks2s3  26860  3cyclfrgrrn1  27149  3cyclfrgrrn  27150  h1de2ctlem  28414  h1de2ci  28415  spansni  28416  spanunsni  28438  riesz3i  28921  adjbd1o  28944  rnbra  28966  pjnmopi  29007  dfpjop  29041  atom1d  29212  cvexchlem  29227  cdj1i  29292  cdj3lem1  29293  hasheuni  30147  cvmlift2lem12  31296  mrsubccat  31415  msrid  31442  elmthm  31473  untint  31589  dfon2lem3  31690  dfon2lem7  31694  dfrdg2  31701  trpred0  31736  nodmon  31803  sltval2  31809  bdayfo  31828  finminlem  32312  fneint  32343  ptrecube  33409  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  zerdivemp1x  33746  dochsnnz  36739  ismrc  37264  eldiophb  37320  eldioph4b  37375  dfacbasgrp  37678  subsaliuncllem  40575  icoresmbl  40757  prmdvdsfmtnof1lem2  41497  sprsymrelfvlem  41740  sprsymrelf1lem  41741  uspgropssxp  41752