Theorem rexlimiv 3148

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  rexlimdv  3153  rexlimivaOLD  3185  rexlimivwOLD  3186  rexlimivv  3199  rexn0OLD  4514  issn  4833  uniss2  4945  disjiun  5135  reuop  6292  ssimaex  6976  ordzsl  7836  onzsl  7837  mpoexw  8067  fsplitfpar  8106  tfrlem8  8386  nneob  8657  ecoptocl  8803  elixpsn  8933  ixpsnf1o  8934  findcard  9165  findcard2  9166  ssfiALT  9176  php  9212  php3  9214  phpOLD  9224  php3OLD  9226  findcard2OLD  9286  ordunifi  9295  fiint  9326  en3lp  9611  inf0  9618  inf3lemd  9624  inf3lem6  9630  noinfep  9657  cantnfvalf  9662  dmttrcl  9718  rnttrcl  9719  ttrclselem1  9722  trcl  9725  bndrank  9838  rankc2  9868  tcrank  9881  ficardom  9958  ac10ct  10031  isinfcard  10089  alephfp  10105  dfac5lem4  10123  dfac2b  10127  ackbij2  10240  fin23lem16  10332  fin23lem29  10338  fin17  10391  fin1a2lem6  10402  itunitc  10418  hsmexlem9  10422  axdc3lem2  10448  axdc3lem4  10450  axcclem  10454  zorn2lem7  10499  wunr1om  10716  tskr1om  10764  grothomex  10826  prnmadd  10994  ltaprlem  11041  mulgt0sr  11102  0cnALT2  11451  renegcli  11523  peano2nn  12226  bndndx  12473  uzn0  12841  ublbneg  12919  om2uzrani  13919  uzrdgfni  13925  exprelprel  14452  rtrclreclem3  15009  rtrclind  15014  rexanuz2  15298  caurcvg  15625  caucvg  15627  infcvgaux1i  15805  vdwlem6  16921  dfgrp2e  18850  efgrelexlemb  19620  cygth  21133  psgnghm  21139  iscldtop  22606  opnneiid  22637  pnfnei  22731  mnfnei  22732  discmp  22909  cmpsublem  22910  cmpfi  22919  2ndcredom  22961  2ndc1stc  22962  2ndcdisj  22967  kgenidm  23058  methaus  24036  xrtgioo  24329  caun0  24805  ovolmge0  25001  itg2lcl  25252  aannenlem2  25849  aannenlem3  25850  aaliou2  25860  2lgslem1b  26902  2sqlem2  26928  ostth  27149  nodmon  27160  sltval2  27166  bdayfo  27187  madef  27359  addsprop  27469  negsprop  27519  mulsprop  27596  elons2  27695  peano2n0s  27711  midwwlks2s3  29244  3cyclfrgrrn1  29576  3cyclfrgrrn  29577  h1de2ctlem  30846  h1de2ci  30847  spansni  30848  spanunsni  30870  riesz3i  31353  adjbd1o  31376  rnbra  31398  pjnmopi  31439  dfpjop  31473  atom1d  31644  cvexchlem  31659  cdj1i  31724  cdj3lem1  31725  hasheuni  33152  cvmlift2lem12  34374  satfrnmapom  34430  sat1el2xp  34439  fmla1  34447  gonar  34455  goalr  34457  fmla0disjsuc  34458  mrsubccat  34578  msrid  34605  elmthm  34636  untint  34750  nnuni  34765  dfon2lem3  34826  dfon2lem7  34830  dfrdg2  34836  finminlem  35289  fneint  35319  ptrecube  36574  poimirlem26  36600  poimirlem27  36601  poimirlem29  36603  poimirlem30  36604  zerdivemp1x  36901  dochsnnz  40407  ismrc  41521  eldiophb  41577  eldioph4b  41631  dfacbasgrp  41932  dfsucon  42356  subsaliuncllem  45152  icoresmbl  45338  elsetpreimafvssdm  46133  sprsymrelfvlem  46237  sprsymrelf1lem  46238  prmdvdsfmtnof1lem2  46332  uspgropssxp  46601  pzriprnglem5  46888  pzriprnglem6  46889  pzriprnglem12  46895  0aryfvalel  47398