Theorem rexlimiv 3146

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  rexlimdv  3151  rexlimivaOLD  3184  rexlimivwOLD  3185  rexlimivv  3199  issn  4837  uniss2  4946  disjiun  5136  reuop  6315  ssimaex  6994  ordzsl  7866  onzsl  7867  mpoexw  8102  fsplitfpar  8142  tfrlem8  8423  nneob  8693  ecoptocl  8846  elixpsn  8976  ixpsnf1o  8977  findcard  9202  findcard2  9203  ssfiALT  9213  php  9245  php3  9247  phpOLD  9257  php3OLD  9259  ordunifi  9324  fiint  9364  fiintOLD  9365  en3lp  9652  inf0  9659  inf3lemd  9665  inf3lem6  9671  noinfep  9698  cantnfvalf  9703  dmttrcl  9759  rnttrcl  9760  ttrclselem1  9763  trcl  9766  bndrank  9879  rankc2  9909  tcrank  9922  ficardom  9999  ac10ct  10072  isinfcard  10130  alephfp  10146  dfac5lem4  10164  dfac5lem4OLD  10166  dfac2b  10169  ackbij2  10280  fin23lem16  10373  fin23lem29  10379  fin17  10432  fin1a2lem6  10443  itunitc  10459  hsmexlem9  10463  axdc3lem2  10489  axdc3lem4  10491  axcclem  10495  zorn2lem7  10540  wunr1om  10757  tskr1om  10805  grothomex  10867  prnmadd  11035  ltaprlem  11082  mulgt0sr  11143  0cnALT2  11495  renegcli  11568  peano2nn  12276  bndndx  12523  uzn0  12893  ublbneg  12973  om2uzrani  13990  uzrdgfni  13996  exprelprel  14526  rtrclreclem3  15096  rtrclind  15101  rexanuz2  15385  caurcvg  15710  caucvg  15712  infcvgaux1i  15890  vdwlem6  17020  dfgrp2e  18994  efgrelexlemb  19783  pzriprnglem5  21514  pzriprnglem6  21515  pzriprnglem12  21521  cygth  21608  psgnghm  21616  iscldtop  23119  opnneiid  23150  pnfnei  23244  mnfnei  23245  discmp  23422  cmpsublem  23423  cmpfi  23432  2ndcredom  23474  2ndc1stc  23475  2ndcdisj  23480  kgenidm  23571  methaus  24549  xrtgioo  24842  caun0  25329  ovolmge0  25526  itg2lcl  25777  aannenlem2  26386  aannenlem3  26387  aaliou2  26397  2lgslem1b  27451  2sqlem2  27477  ostth  27698  nodmon  27710  sltval2  27716  bdayfo  27737  madef  27910  addsprop  28024  negsprop  28082  mulsprop  28171  elons2  28296  nnsge1  28361  dfnns2  28377  n0seo  28420  0reno  28444  remulscllem1  28447  midwwlks2s3  29982  3cyclfrgrrn1  30314  3cyclfrgrrn  30315  h1de2ctlem  31584  h1de2ci  31585  spansni  31586  spanunsni  31608  riesz3i  32091  adjbd1o  32114  rnbra  32136  pjnmopi  32177  dfpjop  32211  atom1d  32382  cvexchlem  32397  cdj1i  32462  cdj3lem1  32463  hasheuni  34066  cvmlift2lem12  35299  satfrnmapom  35355  sat1el2xp  35364  fmla1  35372  gonar  35380  goalr  35382  fmla0disjsuc  35383  mrsubccat  35503  msrid  35530  elmthm  35561  untint  35692  nnuni  35707  dfon2lem3  35767  dfon2lem7  35771  dfrdg2  35777  finminlem  36301  fneint  36331  ptrecube  37607  poimirlem26  37633  poimirlem27  37634  poimirlem29  37636  poimirlem30  37637  zerdivemp1x  37934  dochsnnz  41433  ismrc  42689  eldiophb  42745  eldioph4b  42799  dfacbasgrp  43097  dfsucon  43513  subsaliuncllem  46313  icoresmbl  46499  elsetpreimafvssdm  47311  sprsymrelfvlem  47415  sprsymrelf1lem  47416  prmdvdsfmtnof1lem2  47510  isgrtri  47848  stgredgel  47860  stgr1  47864  uspgropssxp  47988  0aryfvalel  48484