Theorem rexlimiv 3156

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexlimdv  3161  rexlimivv  3204  issn  4786  uniss2  4901  disjiun  5090  reuop  6296  ssimaex  6971  ordzsl  7857  onzsl  7858  mpoexw  8092  fsplitfpar  8132  tfrlem8  8396  nneob  8669  ecoptocl  8832  elixpsn  8969  ixpsnf1o  8970  findcard  9183  findcard2  9184  ssfiALT  9193  php  9226  php3  9228  ordunifi  9285  fiint  9322  en3lp  9619  inf0  9626  inf3lemd  9632  inf3lem6  9638  noinfep  9665  cantnfvalf  9670  dmttrcl  9726  rnttrcl  9727  ttrclselem1  9730  trcl  9733  bndrank  9858  rankc2  9892  tcrank  9905  ficardom  10046  ac10ct  10117  isinfcard  10175  alephfp  10191  dfac5lem4  10209  dfac2b  10213  ackbij2  10324  fin23lem16  10417  fin23lem29  10423  fin17  10476  fin1a2lem6  10487  itunitc  10503  hsmexlem9  10507  axdc3lem2  10533  axdc3lem4  10535  axcclem  10539  zorn2lem7  10584  wunr1om  10808  tskr1om  10856  grothomex  10918  prnmadd  11086  ltaprlem  11133  mulgt0sr  11194  0cnALT2  11550  renegcli  11623  peano2nn  12351  bndndx  12609  uzn0  12986  ublbneg  13064  om2uzrani  14099  uzrdgfni  14105  exprelprel  14639  rtrclreclem3  15219  rtrclind  15224  rexanuz2  15523  caurcvg  15850  caucvg  15852  infcvgaux1i  16032  vdwlem6  17170  dfgrp2e  19180  efgrelexlemb  19970  pzriprnglem5  21797  pzriprnglem6  21798  pzriprnglem12  21804  cygth  21883  psgnghm  21892  iscldtop  23419  opnneiid  23450  pnfnei  23544  mnfnei  23545  discmp  23722  cmpsublem  23723  cmpfi  23732  2ndcredom  23774  2ndc1stc  23775  2ndcdisj  23781  kgenidm  23872  methaus  24845  xrtgioo  25132  caun0  25608  ovolmge0  25804  itg2lcl  26054  aannenlem2  26662  aannenlem3  26663  aaliou2  26673  2lgslem1b  27725  2sqlem2  27751  ostth  27972  nodmon  28013  ltsval2  28019  bdayfo  28040  madef  28228  addsprop  28368  negsprop  28427  mulsprop  28522  elons2  28650  nnsge1  28735  onsfi  28748  dfnns2  28764  n0seo  28813  bdaypw2n0bnd  28856  remulscllem1  28892  midwwlks2s3  30547  3cyclfrgrrn1  30892  3cyclfrgrrn  30893  h1de2ctlem  32163  h1de2ci  32164  spansni  32165  spanunsni  32187  riesz3i  32670  adjbd1o  32693  rnbra  32715  pjnmopi  32756  dfpjop  32790  atom1d  32961  cvexchlem  32976  cdj1i  33041  cdj3lem1  33042  hasheuni  34764  dfac15  35810  cvmlift2lem12  36166  satfrnmapom  36222  sat1el2xp  36231  fmla1  36239  gonar  36247  goalr  36249  fmla0disjsuc  36250  mrsubccat  36370  msrid  36397  elmthm  36428  untint  36570  nnuni  36585  dfon2lem3  36640  dfon2lem7  36644  dfrdg2  36650  finminlem  37199  fneint  37229  ptrecube  38632  poimirlem26  38658  poimirlem27  38659  poimirlem29  38661  poimirlem30  38662  zerdivemp1x  38975  dochsnnz  42601  ismrc  43806  eldiophb  43862  eldioph4b  43912  dfacbasgrp  44204  dfsucon  44618  orbitcl  46041  subsaliuncllem  47461  icoresmbl  47647  elsetpreimafvssdm  48562  sprsymrelfvlem  48666  sprsymrelf1lem  48667  prmdvdsfmtnof1lem2  48764  isgrtri  49135  stgredgel  49149  stgr1  49153  uspgropssxp  49336  0aryfvalel  49840