Theorem rexlimiv 3149

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimdv  3154  rexlimivaOLD  3186  rexlimivwOLD  3187  rexlimivv  3200  rexn0OLD  4513  issn  4832  uniss2  4944  disjiun  5134  reuop  6289  ssimaex  6972  ordzsl  7829  onzsl  7830  mpoexw  8060  fsplitfpar  8099  tfrlem8  8379  nneob  8651  ecoptocl  8797  elixpsn  8927  ixpsnf1o  8928  findcard  9159  findcard2  9160  ssfiALT  9170  php  9206  php3  9208  phpOLD  9218  php3OLD  9220  findcard2OLD  9280  ordunifi  9289  fiint  9320  en3lp  9605  inf0  9612  inf3lemd  9618  inf3lem6  9624  noinfep  9651  cantnfvalf  9656  dmttrcl  9712  rnttrcl  9713  ttrclselem1  9716  trcl  9719  bndrank  9832  rankc2  9862  tcrank  9875  ficardom  9952  ac10ct  10025  isinfcard  10083  alephfp  10099  dfac5lem4  10117  dfac2b  10121  ackbij2  10234  fin23lem16  10326  fin23lem29  10332  fin17  10385  fin1a2lem6  10396  itunitc  10412  hsmexlem9  10416  axdc3lem2  10442  axdc3lem4  10444  axcclem  10448  zorn2lem7  10493  wunr1om  10710  tskr1om  10758  grothomex  10820  prnmadd  10988  ltaprlem  11035  mulgt0sr  11096  0cnALT2  11445  renegcli  11517  peano2nn  12220  bndndx  12467  uzn0  12835  ublbneg  12913  om2uzrani  13913  uzrdgfni  13919  exprelprel  14446  rtrclreclem3  15003  rtrclind  15008  rexanuz2  15292  caurcvg  15619  caucvg  15621  infcvgaux1i  15799  vdwlem6  16915  dfgrp2e  18844  efgrelexlemb  19611  cygth  21111  psgnghm  21117  iscldtop  22581  opnneiid  22612  pnfnei  22706  mnfnei  22707  discmp  22884  cmpsublem  22885  cmpfi  22894  2ndcredom  22936  2ndc1stc  22937  2ndcdisj  22942  kgenidm  23033  methaus  24011  xrtgioo  24304  caun0  24780  ovolmge0  24976  itg2lcl  25227  aannenlem2  25824  aannenlem3  25825  aaliou2  25835  2lgslem1b  26875  2sqlem2  26901  ostth  27122  nodmon  27133  sltval2  27139  bdayfo  27160  madef  27331  addsprop  27440  negsprop  27489  mulsprop  27566  midwwlks2s3  29186  3cyclfrgrrn1  29518  3cyclfrgrrn  29519  h1de2ctlem  30786  h1de2ci  30787  spansni  30788  spanunsni  30810  riesz3i  31293  adjbd1o  31316  rnbra  31338  pjnmopi  31379  dfpjop  31413  atom1d  31584  cvexchlem  31599  cdj1i  31664  cdj3lem1  31665  hasheuni  33021  cvmlift2lem12  34243  satfrnmapom  34299  sat1el2xp  34308  fmla1  34316  gonar  34324  goalr  34326  fmla0disjsuc  34327  mrsubccat  34447  msrid  34474  elmthm  34505  untint  34619  nnuni  34634  dfon2lem3  34695  dfon2lem7  34699  dfrdg2  34705  finminlem  35141  fneint  35171  ptrecube  36426  poimirlem26  36452  poimirlem27  36453  poimirlem29  36455  poimirlem30  36456  zerdivemp1x  36753  dochsnnz  40259  ismrc  41372  eldiophb  41428  eldioph4b  41482  dfacbasgrp  41783  dfsucon  42207  subsaliuncllem  45008  icoresmbl  45194  elsetpreimafvssdm  45989  sprsymrelfvlem  46093  sprsymrelf1lem  46094  prmdvdsfmtnof1lem2  46188  uspgropssxp  46457  0aryfvalel  47222