Theorem rexlimiv 3158

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 412	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3157	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  rexlimdv  3163  rexlimivv  3206  issn  4795  uniss2  4905  disjiun  5095  reuop  6295  ssimaex  6967  ordzsl  7845  onzsl  7846  mpoexw  8081  fsplitfpar  8119  tfrlem8  8377  nneob  8648  ecoptocl  8811  elixpsn  8948  ixpsnf1o  8949  findcard  9162  findcard2  9163  ssfiALT  9172  php  9205  php3  9207  ordunifi  9264  fiint  9300  en3lp  9597  inf0  9604  inf3lemd  9610  inf3lem6  9616  noinfep  9643  cantnfvalf  9648  dmttrcl  9704  rnttrcl  9705  ttrclselem1  9708  trcl  9711  bndrank  9827  rankc2  9857  tcrank  9870  ficardom  9970  ac10ct  10041  isinfcard  10099  alephfp  10115  dfac5lem4  10133  dfac2b  10137  ackbij2  10248  fin23lem16  10341  fin23lem29  10347  fin17  10400  fin1a2lem6  10411  itunitc  10427  hsmexlem9  10431  axdc3lem2  10457  axdc3lem4  10459  axcclem  10463  zorn2lem7  10508  wunr1om  10732  tskr1om  10780  grothomex  10842  prnmadd  11010  ltaprlem  11057  mulgt0sr  11118  0cnALT2  11474  renegcli  11547  peano2nn  12273  bndndx  12531  uzn0  12908  ublbneg  12986  om2uzrani  14020  uzrdgfni  14026  exprelprel  14559  rtrclreclem3  15137  rtrclind  15142  rexanuz2  15441  caurcvg  15768  caucvg  15770  infcvgaux1i  15950  vdwlem6  17084  dfgrp2e  19093  efgrelexlemb  19883  pzriprnglem5  21704  pzriprnglem6  21705  pzriprnglem12  21711  cygth  21790  psgnghm  21799  iscldtop  23326  opnneiid  23357  pnfnei  23451  mnfnei  23452  discmp  23629  cmpsublem  23630  cmpfi  23639  2ndcredom  23681  2ndc1stc  23682  2ndcdisj  23688  kgenidm  23779  methaus  24752  xrtgioo  25039  caun0  25515  ovolmge0  25711  itg2lcl  25961  aannenlem2  26572  aannenlem3  26573  aaliou2  26583  2lgslem1b  27636  2sqlem2  27662  ostth  27883  nodmon  27894  ltsval2  27900  bdayfo  27921  madef  28109  addsprop  28249  negsprop  28308  mulsprop  28403  elons2  28531  nnsge1  28616  onsfi  28629  dfnns2  28645  n0seo  28694  bdaypw2n0bnd  28737  remulscllem1  28773  midwwlks2s3  30428  3cyclfrgrrn1  30773  3cyclfrgrrn  30774  h1de2ctlem  32044  h1de2ci  32045  spansni  32046  spanunsni  32068  riesz3i  32551  adjbd1o  32574  rnbra  32596  pjnmopi  32637  dfpjop  32671  atom1d  32842  cvexchlem  32857  cdj1i  32922  cdj3lem1  32923  hasheuni  34603  cvmlift2lem12  35901  satfrnmapom  35957  sat1el2xp  35966  fmla1  35974  gonar  35982  goalr  35984  fmla0disjsuc  35985  mrsubccat  36105  msrid  36132  elmthm  36163  untint  36299  nnuni  36314  dfon2lem3  36370  dfon2lem7  36374  dfrdg2  36380  finminlem  36945  fneint  36975  ptrecube  38377  poimirlem26  38403  poimirlem27  38404  poimirlem29  38406  poimirlem30  38407  zerdivemp1x  38705  dochsnnz  42331  ismrc  43554  eldiophb  43610  eldioph4b  43660  dfacbasgrp  43957  dfsucon  44371  orbitcl  45788  subsaliuncllem  47193  icoresmbl  47379  elsetpreimafvssdm  48294  sprsymrelfvlem  48398  sprsymrelf1lem  48399  prmdvdsfmtnof1lem2  48496  isgrtri  48867  stgredgel  48881  stgr1  48885  uspgropssxp  49068  0aryfvalel  49572