Theorem rexlimiv 3134

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexlimdv  3139  rexlimivv  3182  issn  4770  uniss2  4879  disjiun  5067  reuop  6251  ssimaex  6919  ordzsl  7792  onzsl  7793  mpoexw  8027  fsplitfpar  8064  tfrlem8  8320  nneob  8589  ecoptocl  8751  elixpsn  8882  ixpsnf1o  8883  findcard  9095  findcard2  9096  ssfiALT  9105  php  9138  php3  9140  ordunifi  9197  fiint  9234  en3lp  9533  inf0  9540  inf3lemd  9546  inf3lem6  9552  noinfep  9579  cantnfvalf  9584  dmttrcl  9640  rnttrcl  9641  ttrclselem1  9644  trcl  9647  bndrank  9763  rankc2  9793  tcrank  9806  ficardom  9883  ac10ct  9954  isinfcard  10012  alephfp  10028  dfac5lem4  10046  dfac5lem4OLD  10048  dfac2b  10051  ackbij2  10162  fin23lem16  10255  fin23lem29  10261  fin17  10314  fin1a2lem6  10325  itunitc  10341  hsmexlem9  10345  axdc3lem2  10371  axdc3lem4  10373  axcclem  10377  zorn2lem7  10422  wunr1om  10640  tskr1om  10688  grothomex  10750  prnmadd  10918  ltaprlem  10965  mulgt0sr  11026  0cnALT2  11380  renegcli  11453  peano2nn  12184  bndndx  12434  uzn0  12803  ublbneg  12881  om2uzrani  13912  uzrdgfni  13918  exprelprel  14450  rtrclreclem3  15020  rtrclind  15025  rexanuz2  15310  caurcvg  15637  caucvg  15639  infcvgaux1i  15820  vdwlem6  16955  dfgrp2e  18937  efgrelexlemb  19723  pzriprnglem5  21467  pzriprnglem6  21468  pzriprnglem12  21474  cygth  21553  psgnghm  21562  iscldtop  23085  opnneiid  23116  pnfnei  23210  mnfnei  23211  discmp  23388  cmpsublem  23389  cmpfi  23398  2ndcredom  23440  2ndc1stc  23441  2ndcdisj  23446  kgenidm  23537  methaus  24510  xrtgioo  24797  caun0  25273  ovolmge0  25469  itg2lcl  25719  aannenlem2  26320  aannenlem3  26321  aaliou2  26331  2lgslem1b  27380  2sqlem2  27406  ostth  27627  nodmon  27639  ltsval2  27645  bdayfo  27666  madef  27853  addsprop  27993  negsprop  28052  mulsprop  28147  elons2  28275  nnsge1  28360  onsfi  28373  dfnns2  28389  n0seo  28438  bdaypw2n0bnd  28481  remulscllem1  28517  midwwlks2s3  30045  3cyclfrgrrn1  30380  3cyclfrgrrn  30381  h1de2ctlem  31651  h1de2ci  31652  spansni  31653  spanunsni  31675  riesz3i  32158  adjbd1o  32181  rnbra  32203  pjnmopi  32244  dfpjop  32278  atom1d  32449  cvexchlem  32464  cdj1i  32529  cdj3lem1  32530  hasheuni  34276  cvmlift2lem12  35549  satfrnmapom  35605  sat1el2xp  35614  fmla1  35622  gonar  35630  goalr  35632  fmla0disjsuc  35633  mrsubccat  35753  msrid  35780  elmthm  35811  untint  35947  nnuni  35962  dfon2lem3  36018  dfon2lem7  36022  dfrdg2  36028  finminlem  36553  fneint  36583  ptrecube  37994  poimirlem26  38020  poimirlem27  38021  poimirlem29  38023  poimirlem30  38024  zerdivemp1x  38321  dochsnnz  41949  ismrc  43157  eldiophb  43213  eldioph4b  43263  dfacbasgrp  43560  dfsucon  43974  orbitcl  45408  subsaliuncllem  46807  icoresmbl  46993  elsetpreimafvssdm  47868  sprsymrelfvlem  47972  sprsymrelf1lem  47973  prmdvdsfmtnof1lem2  48070  isgrtri  48441  stgredgel  48455  stgr1  48459  uspgropssxp  48642  0aryfvalel  49132