Theorem rexlimiv 3130

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

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

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 3061

This theorem is referenced by:  rexlimdv  3135  rexlimivv  3178  issn  4788  uniss2  4897  disjiun  5086  reuop  6251  ssimaex  6919  ordzsl  7787  onzsl  7788  mpoexw  8022  fsplitfpar  8060  tfrlem8  8315  nneob  8584  ecoptocl  8744  elixpsn  8875  ixpsnf1o  8876  findcard  9088  findcard2  9089  ssfiALT  9098  php  9131  php3  9133  ordunifi  9190  fiint  9227  en3lp  9523  inf0  9530  inf3lemd  9536  inf3lem6  9542  noinfep  9569  cantnfvalf  9574  dmttrcl  9630  rnttrcl  9631  ttrclselem1  9634  trcl  9637  bndrank  9753  rankc2  9783  tcrank  9796  ficardom  9873  ac10ct  9944  isinfcard  10002  alephfp  10018  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2b  10041  ackbij2  10152  fin23lem16  10245  fin23lem29  10251  fin17  10304  fin1a2lem6  10315  itunitc  10331  hsmexlem9  10335  axdc3lem2  10361  axdc3lem4  10363  axcclem  10367  zorn2lem7  10412  wunr1om  10630  tskr1om  10678  grothomex  10740  prnmadd  10908  ltaprlem  10955  mulgt0sr  11016  0cnALT2  11369  renegcli  11442  peano2nn  12157  bndndx  12400  uzn0  12768  ublbneg  12846  om2uzrani  13875  uzrdgfni  13881  exprelprel  14413  rtrclreclem3  14983  rtrclind  14988  rexanuz2  15273  caurcvg  15600  caucvg  15602  infcvgaux1i  15780  vdwlem6  16914  dfgrp2e  18893  efgrelexlemb  19679  pzriprnglem5  21440  pzriprnglem6  21441  pzriprnglem12  21447  cygth  21526  psgnghm  21535  iscldtop  23039  opnneiid  23070  pnfnei  23164  mnfnei  23165  discmp  23342  cmpsublem  23343  cmpfi  23352  2ndcredom  23394  2ndc1stc  23395  2ndcdisj  23400  kgenidm  23491  methaus  24464  xrtgioo  24751  caun0  25237  ovolmge0  25434  itg2lcl  25684  aannenlem2  26293  aannenlem3  26294  aaliou2  26304  2lgslem1b  27359  2sqlem2  27385  ostth  27606  nodmon  27618  ltsval2  27624  bdayfo  27645  madef  27832  addsprop  27972  negsprop  28031  mulsprop  28126  elons2  28254  nnsge1  28339  onsfi  28352  dfnns2  28368  n0seo  28417  bdaypw2n0bnd  28460  remulscllem1  28496  midwwlks2s3  30025  3cyclfrgrrn1  30360  3cyclfrgrrn  30361  h1de2ctlem  31630  h1de2ci  31631  spansni  31632  spanunsni  31654  riesz3i  32137  adjbd1o  32160  rnbra  32182  pjnmopi  32223  dfpjop  32257  atom1d  32428  cvexchlem  32443  cdj1i  32508  cdj3lem1  32509  hasheuni  34242  cvmlift2lem12  35508  satfrnmapom  35564  sat1el2xp  35573  fmla1  35581  gonar  35589  goalr  35591  fmla0disjsuc  35592  mrsubccat  35712  msrid  35739  elmthm  35770  untint  35906  nnuni  35921  dfon2lem3  35977  dfon2lem7  35981  dfrdg2  35987  finminlem  36512  fneint  36542  ptrecube  37821  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  poimirlem30  37851  zerdivemp1x  38148  dochsnnz  41710  ismrc  42943  eldiophb  42999  eldioph4b  43053  dfacbasgrp  43350  dfsucon  43764  orbitcl  45198  subsaliuncllem  46601  icoresmbl  46787  elsetpreimafvssdm  47632  sprsymrelfvlem  47736  sprsymrelf1lem  47737  prmdvdsfmtnof1lem2  47831  isgrtri  48189  stgredgel  48203  stgr1  48207  uspgropssxp  48390  0aryfvalel  48880