Theorem rexlimiv 3160

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  rexlimdv  3165  rexlimivv  3208  issn  4790  uniss2  4905  disjiun  5094  reuop  6317  ssimaex  6996  ordzsl  7883  onzsl  7884  mpoexw  8119  fsplitfpar  8159  tfrlem8  8423  nneob  8696  ecoptocl  8859  elixpsn  8996  ixpsnf1o  8997  findcard  9210  findcard2  9211  ssfiALT  9220  php  9253  php3  9255  ordunifi  9312  fiint  9349  en3lp  9645  inf0  9652  inf3lemd  9658  inf3lem6  9664  noinfep  9691  cantnfvalf  9696  dmttrcl  9752  rnttrcl  9753  ttrclselem1  9756  trcl  9759  bndrank  9884  rankc2  9918  tcrank  9931  ficardom  10072  ac10ct  10143  isinfcard  10201  alephfp  10217  dfac5lem4  10235  dfac2b  10239  ackbij2  10350  fin23lem16  10443  fin23lem29  10449  fin17  10502  fin1a2lem6  10513  itunitc  10529  hsmexlem9  10533  axdc3lem2  10559  axdc3lem4  10561  axcclem  10565  zorn2lem7  10610  wunr1om  10834  tskr1om  10882  grothomex  10944  prnmadd  11112  ltaprlem  11159  mulgt0sr  11220  0cnALT2  11576  renegcli  11649  peano2nn  12377  bndndx  12635  uzn0  13012  ublbneg  13090  om2uzrani  14125  uzrdgfni  14131  exprelprel  14665  rtrclreclem3  15245  rtrclind  15250  rexanuz2  15549  caurcvg  15876  caucvg  15878  infcvgaux1i  16058  vdwlem6  17196  dfgrp2e  19206  efgrelexlemb  19997  pzriprnglem5  21824  pzriprnglem6  21825  pzriprnglem12  21831  cygth  21910  psgnghm  21919  iscldtop  23446  opnneiid  23477  pnfnei  23571  mnfnei  23572  discmp  23749  cmpsublem  23750  cmpfi  23759  2ndcredom  23801  2ndc1stc  23802  2ndcdisj  23808  kgenidm  23899  methaus  24872  xrtgioo  25159  caun0  25635  ovolmge0  25831  itg2lcl  26081  aannenlem2  26689  aannenlem3  26690  aaliou2  26700  2lgslem1b  27752  2sqlem2  27778  ostth  27999  nodmon  28040  ltsval2  28046  bdayfo  28067  madef  28255  addsprop  28395  negsprop  28454  mulsprop  28549  elons2  28677  nnsge1  28762  onsfi  28775  dfnns2  28791  n0seo  28840  bdaypw2n0bnd  28883  remulscllem1  28919  midwwlks2s3  30574  3cyclfrgrrn1  30919  3cyclfrgrrn  30920  h1de2ctlem  32190  h1de2ci  32191  spansni  32192  spanunsni  32214  riesz3i  32697  adjbd1o  32720  rnbra  32742  pjnmopi  32783  dfpjop  32817  atom1d  32988  cvexchlem  33003  cdj1i  33068  cdj3lem1  33069  hasheuni  34800  dfac15  35858  cvmlift2lem12  36259  satfrnmapom  36315  sat1el2xp  36324  fmla1  36332  gonar  36340  goalr  36342  fmla0disjsuc  36343  mrsubccat  36463  msrid  36490  elmthm  36521  untint  36668  nnuni  36683  dfon2lem3  36738  dfon2lem7  36742  dfrdg2  36748  finminlem  37297  fneint  37327  ptrecube  38743  poimirlem26  38769  poimirlem27  38770  poimirlem29  38772  poimirlem30  38773  zerdivemp1x  39084  dochsnnz  42710  ismrc  43916  eldiophb  43972  eldioph4b  44022  dfacbasgrp  44313  dfsucon  44727  orbitcl  46153  subsaliuncllem  47582  icoresmbl  47768  elsetpreimafvssdm  48683  sprsymrelfvlem  48787  sprsymrelf1lem  48788  prmdvdsfmtnof1lem2  48885  isgrtri  49256  stgredgel  49270  stgr1  49274  uspgropssxp  49457  0aryfvalel  49961