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  4515  issn  4834  uniss2  4946  disjiun  5136  reuop  6293  ssimaex  6977  ordzsl  7834  onzsl  7835  mpoexw  8065  fsplitfpar  8104  tfrlem8  8384  nneob  8655  ecoptocl  8801  elixpsn  8931  ixpsnf1o  8932  findcard  9163  findcard2  9164  ssfiALT  9174  php  9210  php3  9212  phpOLD  9222  php3OLD  9224  findcard2OLD  9284  ordunifi  9293  fiint  9324  en3lp  9609  inf0  9616  inf3lemd  9622  inf3lem6  9628  noinfep  9655  cantnfvalf  9660  dmttrcl  9716  rnttrcl  9717  ttrclselem1  9720  trcl  9723  bndrank  9836  rankc2  9866  tcrank  9879  ficardom  9956  ac10ct  10029  isinfcard  10087  alephfp  10103  dfac5lem4  10121  dfac2b  10125  ackbij2  10238  fin23lem16  10330  fin23lem29  10336  fin17  10389  fin1a2lem6  10400  itunitc  10416  hsmexlem9  10420  axdc3lem2  10446  axdc3lem4  10448  axcclem  10452  zorn2lem7  10497  wunr1om  10714  tskr1om  10762  grothomex  10824  prnmadd  10992  ltaprlem  11039  mulgt0sr  11100  0cnALT2  11449  renegcli  11521  peano2nn  12224  bndndx  12471  uzn0  12839  ublbneg  12917  om2uzrani  13917  uzrdgfni  13923  exprelprel  14450  rtrclreclem3  15007  rtrclind  15012  rexanuz2  15296  caurcvg  15623  caucvg  15625  infcvgaux1i  15803  vdwlem6  16919  dfgrp2e  18848  efgrelexlemb  19618  cygth  21127  psgnghm  21133  iscldtop  22599  opnneiid  22630  pnfnei  22724  mnfnei  22725  discmp  22902  cmpsublem  22903  cmpfi  22912  2ndcredom  22954  2ndc1stc  22955  2ndcdisj  22960  kgenidm  23051  methaus  24029  xrtgioo  24322  caun0  24798  ovolmge0  24994  itg2lcl  25245  aannenlem2  25842  aannenlem3  25843  aaliou2  25853  2lgslem1b  26895  2sqlem2  26921  ostth  27142  nodmon  27153  sltval2  27159  bdayfo  27180  madef  27351  addsprop  27460  negsprop  27509  mulsprop  27586  midwwlks2s3  29206  3cyclfrgrrn1  29538  3cyclfrgrrn  29539  h1de2ctlem  30808  h1de2ci  30809  spansni  30810  spanunsni  30832  riesz3i  31315  adjbd1o  31338  rnbra  31360  pjnmopi  31401  dfpjop  31435  atom1d  31606  cvexchlem  31621  cdj1i  31686  cdj3lem1  31687  hasheuni  33083  cvmlift2lem12  34305  satfrnmapom  34361  sat1el2xp  34370  fmla1  34378  gonar  34386  goalr  34388  fmla0disjsuc  34389  mrsubccat  34509  msrid  34536  elmthm  34567  untint  34681  nnuni  34696  dfon2lem3  34757  dfon2lem7  34761  dfrdg2  34767  finminlem  35203  fneint  35233  ptrecube  36488  poimirlem26  36514  poimirlem27  36515  poimirlem29  36517  poimirlem30  36518  zerdivemp1x  36815  dochsnnz  40321  ismrc  41439  eldiophb  41495  eldioph4b  41549  dfacbasgrp  41850  dfsucon  42274  subsaliuncllem  45073  icoresmbl  45259  elsetpreimafvssdm  46054  sprsymrelfvlem  46158  sprsymrelf1lem  46159  prmdvdsfmtnof1lem2  46253  uspgropssxp  46522  pzriprnglem5  46809  pzriprnglem6  46810  pzriprnglem12  46816  0aryfvalel  47320