Theorem rexlimiv 3127

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 3126	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  3132  rexlimivaOLD  3164  rexlimivwOLD  3165  rexlimivv  3179  issn  4796  uniss2  4905  disjiun  5095  reuop  6266  ssimaex  6946  ordzsl  7821  onzsl  7822  mpoexw  8057  fsplitfpar  8097  tfrlem8  8352  nneob  8620  ecoptocl  8780  elixpsn  8910  ixpsnf1o  8911  findcard  9127  findcard2  9128  ssfiALT  9138  php  9171  php3  9173  ordunifi  9237  fiint  9277  fiintOLD  9278  en3lp  9567  inf0  9574  inf3lemd  9580  inf3lem6  9586  noinfep  9613  cantnfvalf  9618  dmttrcl  9674  rnttrcl  9675  ttrclselem1  9678  trcl  9681  bndrank  9794  rankc2  9824  tcrank  9837  ficardom  9914  ac10ct  9987  isinfcard  10045  alephfp  10061  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  ackbij2  10195  fin23lem16  10288  fin23lem29  10294  fin17  10347  fin1a2lem6  10358  itunitc  10374  hsmexlem9  10378  axdc3lem2  10404  axdc3lem4  10406  axcclem  10410  zorn2lem7  10455  wunr1om  10672  tskr1om  10720  grothomex  10782  prnmadd  10950  ltaprlem  10997  mulgt0sr  11058  0cnALT2  11410  renegcli  11483  peano2nn  12198  bndndx  12441  uzn0  12810  ublbneg  12892  om2uzrani  13917  uzrdgfni  13923  exprelprel  14455  rtrclreclem3  15026  rtrclind  15031  rexanuz2  15316  caurcvg  15643  caucvg  15645  infcvgaux1i  15823  vdwlem6  16957  dfgrp2e  18895  efgrelexlemb  19680  pzriprnglem5  21395  pzriprnglem6  21396  pzriprnglem12  21402  cygth  21481  psgnghm  21489  iscldtop  22982  opnneiid  23013  pnfnei  23107  mnfnei  23108  discmp  23285  cmpsublem  23286  cmpfi  23295  2ndcredom  23337  2ndc1stc  23338  2ndcdisj  23343  kgenidm  23434  methaus  24408  xrtgioo  24695  caun0  25181  ovolmge0  25378  itg2lcl  25628  aannenlem2  26237  aannenlem3  26238  aaliou2  26248  2lgslem1b  27303  2sqlem2  27329  ostth  27550  nodmon  27562  sltval2  27568  bdayfo  27589  madef  27764  addsprop  27883  negsprop  27941  mulsprop  28033  elons2  28159  nnsge1  28235  onsfi  28247  dfnns2  28261  n0seo  28307  0reno  28348  remulscllem1  28351  midwwlks2s3  29882  3cyclfrgrrn1  30214  3cyclfrgrrn  30215  h1de2ctlem  31484  h1de2ci  31485  spansni  31486  spanunsni  31508  riesz3i  31991  adjbd1o  32014  rnbra  32036  pjnmopi  32077  dfpjop  32111  atom1d  32282  cvexchlem  32297  cdj1i  32362  cdj3lem1  32363  hasheuni  34075  cvmlift2lem12  35301  satfrnmapom  35357  sat1el2xp  35366  fmla1  35374  gonar  35382  goalr  35384  fmla0disjsuc  35385  mrsubccat  35505  msrid  35532  elmthm  35563  untint  35699  nnuni  35714  dfon2lem3  35773  dfon2lem7  35777  dfrdg2  35783  finminlem  36306  fneint  36336  ptrecube  37614  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem30  37644  zerdivemp1x  37941  dochsnnz  41444  ismrc  42689  eldiophb  42745  eldioph4b  42799  dfacbasgrp  43097  dfsucon  43512  orbitcl  44947  subsaliuncllem  46355  icoresmbl  46541  elsetpreimafvssdm  47387  sprsymrelfvlem  47491  sprsymrelf1lem  47492  prmdvdsfmtnof1lem2  47586  isgrtri  47942  stgredgel  47956  stgr1  47960  uspgropssxp  48132  0aryfvalel  48623