Theorem rexlimiv 3131

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  rexlimdv  3136  rexlimivv  3179  issn  4775  uniss2  4884  disjiun  5073  reuop  6257  ssimaex  6925  ordzsl  7796  onzsl  7797  mpoexw  8031  fsplitfpar  8068  tfrlem8  8323  nneob  8592  ecoptocl  8754  elixpsn  8885  ixpsnf1o  8886  findcard  9098  findcard2  9099  ssfiALT  9108  php  9141  php3  9143  ordunifi  9200  fiint  9237  en3lp  9535  inf0  9542  inf3lemd  9548  inf3lem6  9554  noinfep  9581  cantnfvalf  9586  dmttrcl  9642  rnttrcl  9643  ttrclselem1  9646  trcl  9649  bndrank  9765  rankc2  9795  tcrank  9808  ficardom  9885  ac10ct  9956  isinfcard  10014  alephfp  10030  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  ackbij2  10164  fin23lem16  10257  fin23lem29  10263  fin17  10316  fin1a2lem6  10327  itunitc  10343  hsmexlem9  10347  axdc3lem2  10373  axdc3lem4  10375  axcclem  10379  zorn2lem7  10424  wunr1om  10642  tskr1om  10690  grothomex  10752  prnmadd  10920  ltaprlem  10967  mulgt0sr  11028  0cnALT2  11382  renegcli  11455  peano2nn  12186  bndndx  12436  uzn0  12805  ublbneg  12883  om2uzrani  13914  uzrdgfni  13920  exprelprel  14452  rtrclreclem3  15022  rtrclind  15027  rexanuz2  15312  caurcvg  15639  caucvg  15641  infcvgaux1i  15822  vdwlem6  16957  dfgrp2e  18939  efgrelexlemb  19725  pzriprnglem5  21465  pzriprnglem6  21466  pzriprnglem12  21472  cygth  21551  psgnghm  21560  iscldtop  23060  opnneiid  23091  pnfnei  23185  mnfnei  23186  discmp  23363  cmpsublem  23364  cmpfi  23373  2ndcredom  23415  2ndc1stc  23416  2ndcdisj  23421  kgenidm  23512  methaus  24485  xrtgioo  24772  caun0  25248  ovolmge0  25444  itg2lcl  25694  aannenlem2  26295  aannenlem3  26296  aaliou2  26306  2lgslem1b  27355  2sqlem2  27381  ostth  27602  nodmon  27614  ltsval2  27620  bdayfo  27641  madef  27828  addsprop  27968  negsprop  28027  mulsprop  28122  elons2  28250  nnsge1  28335  onsfi  28348  dfnns2  28364  n0seo  28413  bdaypw2n0bnd  28456  remulscllem1  28492  midwwlks2s3  30020  3cyclfrgrrn1  30355  3cyclfrgrrn  30356  h1de2ctlem  31626  h1de2ci  31627  spansni  31628  spanunsni  31650  riesz3i  32133  adjbd1o  32156  rnbra  32178  pjnmopi  32219  dfpjop  32253  atom1d  32424  cvexchlem  32439  cdj1i  32504  cdj3lem1  32505  hasheuni  34229  cvmlift2lem12  35496  satfrnmapom  35552  sat1el2xp  35561  fmla1  35569  gonar  35577  goalr  35579  fmla0disjsuc  35580  mrsubccat  35700  msrid  35727  elmthm  35758  untint  35894  nnuni  35909  dfon2lem3  35965  dfon2lem7  35969  dfrdg2  35975  finminlem  36500  fneint  36530  ptrecube  37941  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem30  37971  zerdivemp1x  38268  dochsnnz  41896  ismrc  43133  eldiophb  43189  eldioph4b  43239  dfacbasgrp  43536  dfsucon  43950  orbitcl  45384  subsaliuncllem  46785  icoresmbl  46971  elsetpreimafvssdm  47846  sprsymrelfvlem  47950  sprsymrelf1lem  47951  prmdvdsfmtnof1lem2  48048  isgrtri  48419  stgredgel  48433  stgr1  48437  uspgropssxp  48620  0aryfvalel  49110