Theorem rexlimiv 3127

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexlimdv  3132  rexlimivv  3175  issn  4785  uniss2  4894  disjiun  5083  reuop  6247  ssimaex  6915  ordzsl  7783  onzsl  7784  mpoexw  8018  fsplitfpar  8056  tfrlem8  8311  nneob  8579  ecoptocl  8739  elixpsn  8869  ixpsnf1o  8870  findcard  9082  findcard2  9083  ssfiALT  9092  php  9125  php3  9127  ordunifi  9183  fiint  9220  en3lp  9513  inf0  9520  inf3lemd  9526  inf3lem6  9532  noinfep  9559  cantnfvalf  9564  dmttrcl  9620  rnttrcl  9621  ttrclselem1  9624  trcl  9627  bndrank  9743  rankc2  9773  tcrank  9786  ficardom  9863  ac10ct  9934  isinfcard  9992  alephfp  10008  dfac5lem4  10026  dfac5lem4OLD  10028  dfac2b  10031  ackbij2  10142  fin23lem16  10235  fin23lem29  10241  fin17  10294  fin1a2lem6  10305  itunitc  10321  hsmexlem9  10325  axdc3lem2  10351  axdc3lem4  10353  axcclem  10357  zorn2lem7  10402  wunr1om  10619  tskr1om  10667  grothomex  10729  prnmadd  10897  ltaprlem  10944  mulgt0sr  11005  0cnALT2  11358  renegcli  11431  peano2nn  12146  bndndx  12389  uzn0  12757  ublbneg  12835  om2uzrani  13863  uzrdgfni  13869  exprelprel  14401  rtrclreclem3  14971  rtrclind  14976  rexanuz2  15261  caurcvg  15588  caucvg  15590  infcvgaux1i  15768  vdwlem6  16902  dfgrp2e  18880  efgrelexlemb  19666  pzriprnglem5  21426  pzriprnglem6  21427  pzriprnglem12  21433  cygth  21512  psgnghm  21521  iscldtop  23013  opnneiid  23044  pnfnei  23138  mnfnei  23139  discmp  23316  cmpsublem  23317  cmpfi  23326  2ndcredom  23368  2ndc1stc  23369  2ndcdisj  23374  kgenidm  23465  methaus  24438  xrtgioo  24725  caun0  25211  ovolmge0  25408  itg2lcl  25658  aannenlem2  26267  aannenlem3  26268  aaliou2  26278  2lgslem1b  27333  2sqlem2  27359  ostth  27580  nodmon  27592  sltval2  27598  bdayfo  27619  madef  27800  addsprop  27922  negsprop  27980  mulsprop  28072  elons2  28198  nnsge1  28274  onsfi  28286  dfnns2  28300  n0seo  28347  0reno  28402  remulscllem1  28405  midwwlks2s3  29934  3cyclfrgrrn1  30269  3cyclfrgrrn  30270  h1de2ctlem  31539  h1de2ci  31540  spansni  31541  spanunsni  31563  riesz3i  32046  adjbd1o  32069  rnbra  32091  pjnmopi  32132  dfpjop  32166  atom1d  32337  cvexchlem  32352  cdj1i  32417  cdj3lem1  32418  hasheuni  34121  cvmlift2lem12  35381  satfrnmapom  35437  sat1el2xp  35446  fmla1  35454  gonar  35462  goalr  35464  fmla0disjsuc  35465  mrsubccat  35585  msrid  35612  elmthm  35643  untint  35779  nnuni  35794  dfon2lem3  35850  dfon2lem7  35854  dfrdg2  35860  finminlem  36385  fneint  36415  ptrecube  37683  poimirlem26  37709  poimirlem27  37710  poimirlem29  37712  poimirlem30  37713  zerdivemp1x  38010  dochsnnz  41572  ismrc  42821  eldiophb  42877  eldioph4b  42931  dfacbasgrp  43228  dfsucon  43643  orbitcl  45077  subsaliuncllem  46482  icoresmbl  46668  elsetpreimafvssdm  47513  sprsymrelfvlem  47617  sprsymrelf1lem  47618  prmdvdsfmtnof1lem2  47712  isgrtri  48070  stgredgel  48084  stgr1  48088  uspgropssxp  48271  0aryfvalel  48762