Theorem rexlimiv 3147

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	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
rexlimiv	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiv

Step	Hyp	Ref	Expression
1		rexlimiv.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	imp 406	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3146	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3070

This theorem is referenced by:  rexlimdv  3152  rexlimivaOLD  3185  rexlimivwOLD  3186  rexlimivv  3200  issn  4831  uniss2  4940  disjiun  5130  reuop  6312  ssimaex  6993  ordzsl  7867  onzsl  7868  mpoexw  8104  fsplitfpar  8144  tfrlem8  8425  nneob  8695  ecoptocl  8848  elixpsn  8978  ixpsnf1o  8979  findcard  9204  findcard2  9205  ssfiALT  9215  php  9248  php3  9250  phpOLD  9260  php3OLD  9262  ordunifi  9327  fiint  9367  fiintOLD  9368  en3lp  9655  inf0  9662  inf3lemd  9668  inf3lem6  9674  noinfep  9701  cantnfvalf  9706  dmttrcl  9762  rnttrcl  9763  ttrclselem1  9766  trcl  9769  bndrank  9882  rankc2  9912  tcrank  9925  ficardom  10002  ac10ct  10075  isinfcard  10133  alephfp  10149  dfac5lem4  10167  dfac5lem4OLD  10169  dfac2b  10172  ackbij2  10283  fin23lem16  10376  fin23lem29  10382  fin17  10435  fin1a2lem6  10446  itunitc  10462  hsmexlem9  10466  axdc3lem2  10492  axdc3lem4  10494  axcclem  10498  zorn2lem7  10543  wunr1om  10760  tskr1om  10808  grothomex  10870  prnmadd  11038  ltaprlem  11085  mulgt0sr  11146  0cnALT2  11498  renegcli  11571  peano2nn  12279  bndndx  12527  uzn0  12896  ublbneg  12976  om2uzrani  13994  uzrdgfni  14000  exprelprel  14530  rtrclreclem3  15100  rtrclind  15105  rexanuz2  15389  caurcvg  15714  caucvg  15716  infcvgaux1i  15894  vdwlem6  17025  dfgrp2e  18982  efgrelexlemb  19769  pzriprnglem5  21497  pzriprnglem6  21498  pzriprnglem12  21504  cygth  21591  psgnghm  21599  iscldtop  23104  opnneiid  23135  pnfnei  23229  mnfnei  23230  discmp  23407  cmpsublem  23408  cmpfi  23417  2ndcredom  23459  2ndc1stc  23460  2ndcdisj  23465  kgenidm  23556  methaus  24534  xrtgioo  24829  caun0  25316  ovolmge0  25513  itg2lcl  25763  aannenlem2  26372  aannenlem3  26373  aaliou2  26383  2lgslem1b  27437  2sqlem2  27463  ostth  27684  nodmon  27696  sltval2  27702  bdayfo  27723  madef  27896  addsprop  28010  negsprop  28068  mulsprop  28157  elons2  28282  nnsge1  28347  dfnns2  28363  n0seo  28406  0reno  28430  remulscllem1  28433  midwwlks2s3  29973  3cyclfrgrrn1  30305  3cyclfrgrrn  30306  h1de2ctlem  31575  h1de2ci  31576  spansni  31577  spanunsni  31599  riesz3i  32082  adjbd1o  32105  rnbra  32127  pjnmopi  32168  dfpjop  32202  atom1d  32373  cvexchlem  32388  cdj1i  32453  cdj3lem1  32454  hasheuni  34087  cvmlift2lem12  35320  satfrnmapom  35376  sat1el2xp  35385  fmla1  35393  gonar  35401  goalr  35403  fmla0disjsuc  35404  mrsubccat  35524  msrid  35551  elmthm  35582  untint  35713  nnuni  35728  dfon2lem3  35787  dfon2lem7  35791  dfrdg2  35797  finminlem  36320  fneint  36350  ptrecube  37628  poimirlem26  37654  poimirlem27  37655  poimirlem29  37657  poimirlem30  37658  zerdivemp1x  37955  dochsnnz  41453  ismrc  42717  eldiophb  42773  eldioph4b  42827  dfacbasgrp  43125  dfsucon  43541  subsaliuncllem  46377  icoresmbl  46563  elsetpreimafvssdm  47378  sprsymrelfvlem  47482  sprsymrelf1lem  47483  prmdvdsfmtnof1lem2  47577  isgrtri  47915  stgredgel  47929  stgr1  47933  uspgropssxp  48065  0aryfvalel  48560