Theorem rexlimiv 3123

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdv  3128  rexlimivv  3171  issn  4786  uniss2  4894  disjiun  5083  reuop  6245  ssimaex  6912  ordzsl  7785  onzsl  7786  mpoexw  8020  fsplitfpar  8058  tfrlem8  8313  nneob  8581  ecoptocl  8741  elixpsn  8871  ixpsnf1o  8872  findcard  9087  findcard2  9088  ssfiALT  9098  php  9131  php3  9133  ordunifi  9195  fiint  9235  fiintOLD  9236  en3lp  9529  inf0  9536  inf3lemd  9542  inf3lem6  9548  noinfep  9575  cantnfvalf  9580  dmttrcl  9636  rnttrcl  9637  ttrclselem1  9640  trcl  9643  bndrank  9756  rankc2  9786  tcrank  9799  ficardom  9876  ac10ct  9947  isinfcard  10005  alephfp  10021  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  ackbij2  10155  fin23lem16  10248  fin23lem29  10254  fin17  10307  fin1a2lem6  10318  itunitc  10334  hsmexlem9  10338  axdc3lem2  10364  axdc3lem4  10366  axcclem  10370  zorn2lem7  10415  wunr1om  10632  tskr1om  10680  grothomex  10742  prnmadd  10910  ltaprlem  10957  mulgt0sr  11018  0cnALT2  11370  renegcli  11443  peano2nn  12158  bndndx  12401  uzn0  12770  ublbneg  12852  om2uzrani  13877  uzrdgfni  13883  exprelprel  14415  rtrclreclem3  14985  rtrclind  14990  rexanuz2  15275  caurcvg  15602  caucvg  15604  infcvgaux1i  15782  vdwlem6  16916  dfgrp2e  18860  efgrelexlemb  19647  pzriprnglem5  21410  pzriprnglem6  21411  pzriprnglem12  21417  cygth  21496  psgnghm  21505  iscldtop  22998  opnneiid  23029  pnfnei  23123  mnfnei  23124  discmp  23301  cmpsublem  23302  cmpfi  23311  2ndcredom  23353  2ndc1stc  23354  2ndcdisj  23359  kgenidm  23450  methaus  24424  xrtgioo  24711  caun0  25197  ovolmge0  25394  itg2lcl  25644  aannenlem2  26253  aannenlem3  26254  aaliou2  26264  2lgslem1b  27319  2sqlem2  27345  ostth  27566  nodmon  27578  sltval2  27584  bdayfo  27605  madef  27784  addsprop  27906  negsprop  27964  mulsprop  28056  elons2  28182  nnsge1  28258  onsfi  28270  dfnns2  28284  n0seo  28331  0reno  28384  remulscllem1  28387  midwwlks2s3  29915  3cyclfrgrrn1  30247  3cyclfrgrrn  30248  h1de2ctlem  31517  h1de2ci  31518  spansni  31519  spanunsni  31541  riesz3i  32024  adjbd1o  32047  rnbra  32069  pjnmopi  32110  dfpjop  32144  atom1d  32315  cvexchlem  32330  cdj1i  32395  cdj3lem1  32396  hasheuni  34054  cvmlift2lem12  35289  satfrnmapom  35345  sat1el2xp  35354  fmla1  35362  gonar  35370  goalr  35372  fmla0disjsuc  35373  mrsubccat  35493  msrid  35520  elmthm  35551  untint  35687  nnuni  35702  dfon2lem3  35761  dfon2lem7  35765  dfrdg2  35771  finminlem  36294  fneint  36324  ptrecube  37602  poimirlem26  37628  poimirlem27  37629  poimirlem29  37631  poimirlem30  37632  zerdivemp1x  37929  dochsnnz  41432  ismrc  42677  eldiophb  42733  eldioph4b  42787  dfacbasgrp  43084  dfsucon  43499  orbitcl  44934  subsaliuncllem  46342  icoresmbl  46528  elsetpreimafvssdm  47374  sprsymrelfvlem  47478  sprsymrelf1lem  47479  prmdvdsfmtnof1lem2  47573  isgrtri  47931  stgredgel  47945  stgr1  47949  uspgropssxp  48132  0aryfvalel  48623