Theorem rexlimiv 3132

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimdv  3137  rexlimivv  3180  issn  4776  uniss2  4885  disjiun  5074  reuop  6251  ssimaex  6919  ordzsl  7789  onzsl  7790  mpoexw  8024  fsplitfpar  8061  tfrlem8  8316  nneob  8585  ecoptocl  8747  elixpsn  8878  ixpsnf1o  8879  findcard  9091  findcard2  9092  ssfiALT  9101  php  9134  php3  9136  ordunifi  9193  fiint  9230  en3lp  9526  inf0  9533  inf3lemd  9539  inf3lem6  9545  noinfep  9572  cantnfvalf  9577  dmttrcl  9633  rnttrcl  9634  ttrclselem1  9637  trcl  9640  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  10633  tskr1om  10681  grothomex  10743  prnmadd  10911  ltaprlem  10958  mulgt0sr  11019  0cnALT2  11373  renegcli  11446  peano2nn  12177  bndndx  12427  uzn0  12796  ublbneg  12874  om2uzrani  13905  uzrdgfni  13911  exprelprel  14443  rtrclreclem3  15013  rtrclind  15018  rexanuz2  15303  caurcvg  15630  caucvg  15632  infcvgaux1i  15813  vdwlem6  16948  dfgrp2e  18930  efgrelexlemb  19716  pzriprnglem5  21475  pzriprnglem6  21476  pzriprnglem12  21482  cygth  21561  psgnghm  21570  iscldtop  23070  opnneiid  23101  pnfnei  23195  mnfnei  23196  discmp  23373  cmpsublem  23374  cmpfi  23383  2ndcredom  23425  2ndc1stc  23426  2ndcdisj  23431  kgenidm  23522  methaus  24495  xrtgioo  24782  caun0  25258  ovolmge0  25454  itg2lcl  25704  aannenlem2  26306  aannenlem3  26307  aaliou2  26317  2lgslem1b  27369  2sqlem2  27395  ostth  27616  nodmon  27628  ltsval2  27634  bdayfo  27655  madef  27842  addsprop  27982  negsprop  28041  mulsprop  28136  elons2  28264  nnsge1  28349  onsfi  28362  dfnns2  28378  n0seo  28427  bdaypw2n0bnd  28470  remulscllem1  28506  midwwlks2s3  30035  3cyclfrgrrn1  30370  3cyclfrgrrn  30371  h1de2ctlem  31641  h1de2ci  31642  spansni  31643  spanunsni  31665  riesz3i  32148  adjbd1o  32171  rnbra  32193  pjnmopi  32234  dfpjop  32268  atom1d  32439  cvexchlem  32454  cdj1i  32519  cdj3lem1  32520  hasheuni  34245  cvmlift2lem12  35512  satfrnmapom  35568  sat1el2xp  35577  fmla1  35585  gonar  35593  goalr  35595  fmla0disjsuc  35596  mrsubccat  35716  msrid  35743  elmthm  35774  untint  35910  nnuni  35925  dfon2lem3  35981  dfon2lem7  35985  dfrdg2  35991  finminlem  36516  fneint  36546  ptrecube  37955  poimirlem26  37981  poimirlem27  37982  poimirlem29  37984  poimirlem30  37985  zerdivemp1x  38282  dochsnnz  41910  ismrc  43147  eldiophb  43203  eldioph4b  43257  dfacbasgrp  43554  dfsucon  43968  orbitcl  45402  subsaliuncllem  46803  icoresmbl  46989  elsetpreimafvssdm  47858  sprsymrelfvlem  47962  sprsymrelf1lem  47963  prmdvdsfmtnof1lem2  48060  isgrtri  48431  stgredgel  48445  stgr1  48449  uspgropssxp  48632  0aryfvalel  49122