Theorem rexlimiv 3157

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

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

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 3088

This theorem is used by:  rexlimdv  3162  rexlimivv  3205  issn  4792  uniss2  4902  disjiun  5091  reuop  6289  ssimaex  6962  ordzsl  7845  onzsl  7846  mpoexw  8080  fsplitfpar  8118  tfrlem8  8376  nneob  8649  ecoptocl  8812  elixpsn  8949  ixpsnf1o  8950  findcard  9163  findcard2  9164  ssfiALT  9173  php  9206  php3  9208  ordunifi  9265  fiint  9302  en3lp  9599  inf0  9606  inf3lemd  9612  inf3lem6  9618  noinfep  9645  cantnfvalf  9650  dmttrcl  9706  rnttrcl  9707  ttrclselem1  9710  trcl  9713  bndrank  9835  rankc2  9869  tcrank  9882  ficardom  10023  ac10ct  10094  isinfcard  10152  alephfp  10168  dfac5lem4  10186  dfac2b  10190  ackbij2  10301  fin23lem16  10394  fin23lem29  10400  fin17  10453  fin1a2lem6  10464  itunitc  10480  hsmexlem9  10484  axdc3lem2  10510  axdc3lem4  10512  axcclem  10516  zorn2lem7  10561  wunr1om  10785  tskr1om  10833  grothomex  10895  prnmadd  11063  ltaprlem  11110  mulgt0sr  11171  0cnALT2  11527  renegcli  11600  peano2nn  12328  bndndx  12586  uzn0  12963  ublbneg  13041  om2uzrani  14075  uzrdgfni  14081  exprelprel  14615  rtrclreclem3  15193  rtrclind  15198  rexanuz2  15497  caurcvg  15824  caucvg  15826  infcvgaux1i  16006  vdwlem6  17144  dfgrp2e  19154  efgrelexlemb  19944  pzriprnglem5  21771  pzriprnglem6  21772  pzriprnglem12  21778  cygth  21857  psgnghm  21866  iscldtop  23393  opnneiid  23424  pnfnei  23518  mnfnei  23519  discmp  23696  cmpsublem  23697  cmpfi  23706  2ndcredom  23748  2ndc1stc  23749  2ndcdisj  23755  kgenidm  23846  methaus  24819  xrtgioo  25106  caun0  25582  ovolmge0  25778  itg2lcl  26028  aannenlem2  26638  aannenlem3  26639  aaliou2  26649  2lgslem1b  27701  2sqlem2  27727  ostth  27948  nodmon  27989  ltsval2  27995  bdayfo  28016  madef  28204  addsprop  28344  negsprop  28403  mulsprop  28498  elons2  28626  nnsge1  28711  onsfi  28724  dfnns2  28740  n0seo  28789  bdaypw2n0bnd  28832  remulscllem1  28868  midwwlks2s3  30523  3cyclfrgrrn1  30868  3cyclfrgrrn  30869  h1de2ctlem  32139  h1de2ci  32140  spansni  32141  spanunsni  32163  riesz3i  32646  adjbd1o  32669  rnbra  32691  pjnmopi  32732  dfpjop  32766  atom1d  32937  cvexchlem  32952  cdj1i  33017  cdj3lem1  33018  hasheuni  34699  cvmlift2lem12  36048  satfrnmapom  36104  sat1el2xp  36113  fmla1  36121  gonar  36129  goalr  36131  fmla0disjsuc  36132  mrsubccat  36252  msrid  36279  elmthm  36310  untint  36446  nnuni  36461  dfon2lem3  36517  dfon2lem7  36521  dfrdg2  36527  finminlem  37076  fneint  37106  ptrecube  38506  poimirlem26  38532  poimirlem27  38533  poimirlem29  38535  poimirlem30  38536  zerdivemp1x  38849  dochsnnz  42475  ismrc  43665  eldiophb  43721  eldioph4b  43771  dfacbasgrp  44068  dfsucon  44482  orbitcl  45899  subsaliuncllem  47311  icoresmbl  47497  elsetpreimafvssdm  48412  sprsymrelfvlem  48516  sprsymrelf1lem  48517  prmdvdsfmtnof1lem2  48614  isgrtri  48985  stgredgel  48999  stgr1  49003  uspgropssxp  49186  0aryfvalel  49690