Theorem rexlimiv 3135

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3062

This theorem is referenced by:  rexlimdv  3140  rexlimivaOLD  3172  rexlimivwOLD  3173  rexlimivv  3187  issn  4813  uniss2  4922  disjiun  5112  reuop  6287  ssimaex  6969  ordzsl  7845  onzsl  7846  mpoexw  8082  fsplitfpar  8122  tfrlem8  8403  nneob  8673  ecoptocl  8826  elixpsn  8956  ixpsnf1o  8957  findcard  9182  findcard2  9183  ssfiALT  9193  php  9226  php3  9228  phpOLD  9236  php3OLD  9238  ordunifi  9303  fiint  9343  fiintOLD  9344  en3lp  9633  inf0  9640  inf3lemd  9646  inf3lem6  9652  noinfep  9679  cantnfvalf  9684  dmttrcl  9740  rnttrcl  9741  ttrclselem1  9744  trcl  9747  bndrank  9860  rankc2  9890  tcrank  9903  ficardom  9980  ac10ct  10053  isinfcard  10111  alephfp  10127  dfac5lem4  10145  dfac5lem4OLD  10147  dfac2b  10150  ackbij2  10261  fin23lem16  10354  fin23lem29  10360  fin17  10413  fin1a2lem6  10424  itunitc  10440  hsmexlem9  10444  axdc3lem2  10470  axdc3lem4  10472  axcclem  10476  zorn2lem7  10521  wunr1om  10738  tskr1om  10786  grothomex  10848  prnmadd  11016  ltaprlem  11063  mulgt0sr  11124  0cnALT2  11476  renegcli  11549  peano2nn  12257  bndndx  12505  uzn0  12874  ublbneg  12954  om2uzrani  13975  uzrdgfni  13981  exprelprel  14513  rtrclreclem3  15084  rtrclind  15089  rexanuz2  15373  caurcvg  15698  caucvg  15700  infcvgaux1i  15878  vdwlem6  17011  dfgrp2e  18951  efgrelexlemb  19736  pzriprnglem5  21451  pzriprnglem6  21452  pzriprnglem12  21458  cygth  21537  psgnghm  21545  iscldtop  23038  opnneiid  23069  pnfnei  23163  mnfnei  23164  discmp  23341  cmpsublem  23342  cmpfi  23351  2ndcredom  23393  2ndc1stc  23394  2ndcdisj  23399  kgenidm  23490  methaus  24464  xrtgioo  24751  caun0  25238  ovolmge0  25435  itg2lcl  25685  aannenlem2  26294  aannenlem3  26295  aaliou2  26305  2lgslem1b  27360  2sqlem2  27386  ostth  27607  nodmon  27619  sltval2  27625  bdayfo  27646  madef  27821  addsprop  27940  negsprop  27998  mulsprop  28090  elons2  28216  nnsge1  28292  onsfi  28304  dfnns2  28318  n0seo  28364  0reno  28405  remulscllem1  28408  midwwlks2s3  29939  3cyclfrgrrn1  30271  3cyclfrgrrn  30272  h1de2ctlem  31541  h1de2ci  31542  spansni  31543  spanunsni  31565  riesz3i  32048  adjbd1o  32071  rnbra  32093  pjnmopi  32134  dfpjop  32168  atom1d  32339  cvexchlem  32354  cdj1i  32419  cdj3lem1  32420  hasheuni  34121  cvmlift2lem12  35341  satfrnmapom  35397  sat1el2xp  35406  fmla1  35414  gonar  35422  goalr  35424  fmla0disjsuc  35425  mrsubccat  35545  msrid  35572  elmthm  35603  untint  35734  nnuni  35749  dfon2lem3  35808  dfon2lem7  35812  dfrdg2  35818  finminlem  36341  fneint  36371  ptrecube  37649  poimirlem26  37675  poimirlem27  37676  poimirlem29  37678  poimirlem30  37679  zerdivemp1x  37976  dochsnnz  41474  ismrc  42699  eldiophb  42755  eldioph4b  42809  dfacbasgrp  43107  dfsucon  43522  orbitcl  44957  subsaliuncllem  46366  icoresmbl  46552  elsetpreimafvssdm  47380  sprsymrelfvlem  47484  sprsymrelf1lem  47485  prmdvdsfmtnof1lem2  47579  isgrtri  47935  stgredgel  47949  stgr1  47953  uspgropssxp  48099  0aryfvalel  48594