Theorem rexlimiv 3159

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimdv  3164  rexlimivv  3207  issn  4798  uniss2  4908  disjiun  5098  reuop  6296  ssimaex  6968  ordzsl  7842  onzsl  7843  mpoexw  8076  fsplitfpar  8114  tfrlem8  8372  nneob  8643  ecoptocl  8806  elixpsn  8936  ixpsnf1o  8937  findcard  9149  findcard2  9150  ssfiALT  9159  php  9192  php3  9194  ordunifi  9251  fiint  9287  en3lp  9584  inf0  9591  inf3lemd  9597  inf3lem6  9603  noinfep  9630  cantnfvalf  9635  dmttrcl  9691  rnttrcl  9692  ttrclselem1  9695  trcl  9698  bndrank  9814  rankc2  9844  tcrank  9857  ficardom  9948  ac10ct  10019  isinfcard  10077  alephfp  10093  dfac5lem4  10111  dfac2b  10115  ackbij2  10226  fin23lem16  10320  fin23lem29  10326  fin17  10379  fin1a2lem6  10390  itunitc  10406  hsmexlem9  10410  axdc3lem2  10436  axdc3lem4  10438  axcclem  10442  zorn2lem7  10487  wunr1om  10705  tskr1om  10753  grothomex  10815  prnmadd  10983  ltaprlem  11030  mulgt0sr  11091  0cnALT2  11447  renegcli  11520  peano2nn  12246  bndndx  12504  uzn0  12880  ublbneg  12958  om2uzrani  13990  uzrdgfni  13996  exprelprel  14529  rtrclreclem3  15099  rtrclind  15104  rexanuz2  15403  caurcvg  15730  caucvg  15732  infcvgaux1i  15913  vdwlem6  17047  dfgrp2e  19031  efgrelexlemb  19821  pzriprnglem5  21616  pzriprnglem6  21617  pzriprnglem12  21623  cygth  21702  psgnghm  21711  iscldtop  23233  opnneiid  23264  pnfnei  23358  mnfnei  23359  discmp  23536  cmpsublem  23537  cmpfi  23546  2ndcredom  23588  2ndc1stc  23589  2ndcdisj  23594  kgenidm  23685  methaus  24658  xrtgioo  24945  caun0  25421  ovolmge0  25617  itg2lcl  25867  aannenlem2  26473  aannenlem3  26474  aaliou2  26484  2lgslem1b  27537  2sqlem2  27563  ostth  27784  nodmon  27795  ltsval2  27801  bdayfo  27822  madef  28010  addsprop  28150  negsprop  28209  mulsprop  28304  elons2  28432  nnsge1  28517  onsfi  28530  dfnns2  28546  n0seo  28595  bdaypw2n0bnd  28638  remulscllem1  28674  midwwlks2s3  30282  3cyclfrgrrn1  30617  3cyclfrgrrn  30618  h1de2ctlem  31888  h1de2ci  31889  spansni  31890  spanunsni  31912  riesz3i  32395  adjbd1o  32418  rnbra  32440  pjnmopi  32481  dfpjop  32515  atom1d  32686  cvexchlem  32701  cdj1i  32766  cdj3lem1  32767  hasheuni  34456  cvmlift2lem12  35787  satfrnmapom  35843  sat1el2xp  35852  fmla1  35860  gonar  35868  goalr  35870  fmla0disjsuc  35871  mrsubccat  35991  msrid  36018  elmthm  36049  untint  36185  nnuni  36200  dfon2lem3  36256  dfon2lem7  36260  dfrdg2  36266  finminlem  36810  fneint  36840  ptrecube  38252  poimirlem26  38278  poimirlem27  38279  poimirlem29  38281  poimirlem30  38282  zerdivemp1x  38579  dochsnnz  42205  ismrc  43415  eldiophb  43471  eldioph4b  43521  dfacbasgrp  43818  dfsucon  44232  orbitcl  45649  subsaliuncllem  47054  icoresmbl  47240  elsetpreimafvssdm  48118  sprsymrelfvlem  48222  sprsymrelf1lem  48223  prmdvdsfmtnof1lem2  48320  isgrtri  48691  stgredgel  48705  stgr1  48709  uspgropssxp  48892  0aryfvalel  49397