Theorem rexlimiv 3155

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexlimdv  3160  rexlimivv  3203  issn  4787  uniss2  4897  disjiun  5085  reuop  6274  ssimaex  6946  ordzsl  7819  onzsl  7820  mpoexw  8053  fsplitfpar  8090  tfrlem8  8348  nneob  8619  ecoptocl  8782  elixpsn  8912  ixpsnf1o  8913  findcard  9125  findcard2  9126  ssfiALT  9135  php  9168  php3  9170  ordunifi  9227  fiint  9264  en3lp  9562  inf0  9569  inf3lemd  9575  inf3lem6  9581  noinfep  9608  cantnfvalf  9613  dmttrcl  9669  rnttrcl  9670  ttrclselem1  9673  trcl  9676  bndrank  9792  rankc2  9822  tcrank  9835  ficardom  9912  ac10ct  9983  isinfcard  10041  alephfp  10057  dfac5lem4  10075  dfac5lem4OLD  10077  dfac2b  10080  ackbij2  10191  fin23lem16  10285  fin23lem29  10291  fin17  10344  fin1a2lem6  10355  itunitc  10371  hsmexlem9  10375  axdc3lem2  10401  axdc3lem4  10403  axcclem  10407  zorn2lem7  10452  wunr1om  10670  tskr1om  10718  grothomex  10780  prnmadd  10948  ltaprlem  10995  mulgt0sr  11056  0cnALT2  11412  renegcli  11485  peano2nn  12215  bndndx  12473  uzn0  12849  ublbneg  12927  om2uzrani  13958  uzrdgfni  13964  exprelprel  14496  rtrclreclem3  15066  rtrclind  15071  rexanuz2  15367  caurcvg  15694  caucvg  15696  infcvgaux1i  15877  vdwlem6  17012  dfgrp2e  18995  efgrelexlemb  19780  pzriprnglem5  21524  pzriprnglem6  21525  pzriprnglem12  21531  cygth  21610  psgnghm  21619  iscldtop  23142  opnneiid  23173  pnfnei  23267  mnfnei  23268  discmp  23445  cmpsublem  23446  cmpfi  23455  2ndcredom  23497  2ndc1stc  23498  2ndcdisj  23503  kgenidm  23594  methaus  24567  xrtgioo  24854  caun0  25330  ovolmge0  25526  itg2lcl  25776  aannenlem2  26380  aannenlem3  26381  aaliou2  26391  2lgslem1b  27443  2sqlem2  27469  ostth  27690  nodmon  27701  ltsval2  27707  bdayfo  27728  madef  27916  addsprop  28056  negsprop  28115  mulsprop  28210  elons2  28338  nnsge1  28423  onsfi  28436  dfnns2  28452  n0seo  28501  bdaypw2n0bnd  28544  remulscllem1  28580  midwwlks2s3  30108  3cyclfrgrrn1  30443  3cyclfrgrrn  30444  h1de2ctlem  31714  h1de2ci  31715  spansni  31716  spanunsni  31738  riesz3i  32221  adjbd1o  32244  rnbra  32266  pjnmopi  32307  dfpjop  32341  atom1d  32512  cvexchlem  32527  cdj1i  32592  cdj3lem1  32593  hasheuni  34342  cvmlift2lem12  35624  satfrnmapom  35680  sat1el2xp  35689  fmla1  35697  gonar  35705  goalr  35707  fmla0disjsuc  35708  mrsubccat  35828  msrid  35855  elmthm  35886  untint  36022  nnuni  36037  dfon2lem3  36093  dfon2lem7  36097  dfrdg2  36103  finminlem  36638  fneint  36668  ptrecube  38079  poimirlem26  38105  poimirlem27  38106  poimirlem29  38108  poimirlem30  38109  zerdivemp1x  38406  dochsnnz  42034  ismrc  43242  eldiophb  43298  eldioph4b  43348  dfacbasgrp  43645  dfsucon  44059  orbitcl  45493  subsaliuncllem  46891  icoresmbl  47077  elsetpreimafvssdm  47952  sprsymrelfvlem  48056  sprsymrelf1lem  48057  prmdvdsfmtnof1lem2  48154  isgrtri  48525  stgredgel  48539  stgr1  48543  uspgropssxp  48726  0aryfvalel  49216