Theorem rexlimiv 3126

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  rexlimdv  3131  rexlimivv  3174  issn  4781  uniss2  4890  disjiun  5077  reuop  6240  ssimaex  6907  ordzsl  7775  onzsl  7776  mpoexw  8010  fsplitfpar  8048  tfrlem8  8303  nneob  8571  ecoptocl  8731  elixpsn  8861  ixpsnf1o  8862  findcard  9073  findcard2  9074  ssfiALT  9083  php  9116  php3  9118  ordunifi  9174  fiint  9211  en3lp  9504  inf0  9511  inf3lemd  9517  inf3lem6  9523  noinfep  9550  cantnfvalf  9555  dmttrcl  9611  rnttrcl  9612  ttrclselem1  9615  trcl  9618  bndrank  9734  rankc2  9764  tcrank  9777  ficardom  9854  ac10ct  9925  isinfcard  9983  alephfp  9999  dfac5lem4  10017  dfac5lem4OLD  10019  dfac2b  10022  ackbij2  10133  fin23lem16  10226  fin23lem29  10232  fin17  10285  fin1a2lem6  10296  itunitc  10312  hsmexlem9  10316  axdc3lem2  10342  axdc3lem4  10344  axcclem  10348  zorn2lem7  10393  wunr1om  10610  tskr1om  10658  grothomex  10720  prnmadd  10888  ltaprlem  10935  mulgt0sr  10996  0cnALT2  11349  renegcli  11422  peano2nn  12137  bndndx  12380  uzn0  12749  ublbneg  12831  om2uzrani  13859  uzrdgfni  13865  exprelprel  14397  rtrclreclem3  14967  rtrclind  14972  rexanuz2  15257  caurcvg  15584  caucvg  15586  infcvgaux1i  15764  vdwlem6  16898  dfgrp2e  18876  efgrelexlemb  19662  pzriprnglem5  21422  pzriprnglem6  21423  pzriprnglem12  21429  cygth  21508  psgnghm  21517  iscldtop  23010  opnneiid  23041  pnfnei  23135  mnfnei  23136  discmp  23313  cmpsublem  23314  cmpfi  23323  2ndcredom  23365  2ndc1stc  23366  2ndcdisj  23371  kgenidm  23462  methaus  24435  xrtgioo  24722  caun0  25208  ovolmge0  25405  itg2lcl  25655  aannenlem2  26264  aannenlem3  26265  aaliou2  26275  2lgslem1b  27330  2sqlem2  27356  ostth  27577  nodmon  27589  sltval2  27595  bdayfo  27616  madef  27797  addsprop  27919  negsprop  27977  mulsprop  28069  elons2  28195  nnsge1  28271  onsfi  28283  dfnns2  28297  n0seo  28344  0reno  28399  remulscllem1  28402  midwwlks2s3  29930  3cyclfrgrrn1  30265  3cyclfrgrrn  30266  h1de2ctlem  31535  h1de2ci  31536  spansni  31537  spanunsni  31559  riesz3i  32042  adjbd1o  32065  rnbra  32087  pjnmopi  32128  dfpjop  32162  atom1d  32333  cvexchlem  32348  cdj1i  32413  cdj3lem1  32414  hasheuni  34098  cvmlift2lem12  35358  satfrnmapom  35414  sat1el2xp  35423  fmla1  35431  gonar  35439  goalr  35441  fmla0disjsuc  35442  mrsubccat  35562  msrid  35589  elmthm  35620  untint  35756  nnuni  35771  dfon2lem3  35827  dfon2lem7  35831  dfrdg2  35837  finminlem  36362  fneint  36392  ptrecube  37659  poimirlem26  37685  poimirlem27  37686  poimirlem29  37688  poimirlem30  37689  zerdivemp1x  37986  dochsnnz  41548  ismrc  42793  eldiophb  42849  eldioph4b  42903  dfacbasgrp  43200  dfsucon  43615  orbitcl  45049  subsaliuncllem  46454  icoresmbl  46640  elsetpreimafvssdm  47485  sprsymrelfvlem  47589  sprsymrelf1lem  47590  prmdvdsfmtnof1lem2  47684  isgrtri  48042  stgredgel  48056  stgr1  48060  uspgropssxp  48243  0aryfvalel  48734