Theorem rexlimiv 3149

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimdv  3154  rexlimivaOLD  3186  rexlimivwOLD  3187  rexlimivv  3200  rexn0OLD  4510  issn  4829  uniss2  4941  disjiun  5131  reuop  6284  ssimaex  6965  ordzsl  7821  onzsl  7822  mpoexw  8052  fsplitfpar  8091  tfrlem8  8371  nneob  8643  ecoptocl  8789  elixpsn  8919  ixpsnf1o  8920  findcard  9151  findcard2  9152  ssfiALT  9162  php  9198  php3  9200  phpOLD  9210  php3OLD  9212  findcard2OLD  9272  ordunifi  9281  fiint  9312  en3lp  9596  inf0  9603  inf3lemd  9609  inf3lem6  9615  noinfep  9642  cantnfvalf  9647  dmttrcl  9703  rnttrcl  9704  ttrclselem1  9707  trcl  9710  bndrank  9823  rankc2  9853  tcrank  9866  ficardom  9943  ac10ct  10016  isinfcard  10074  alephfp  10090  dfac5lem4  10108  dfac2b  10112  ackbij2  10225  fin23lem16  10317  fin23lem29  10323  fin17  10376  fin1a2lem6  10387  itunitc  10403  hsmexlem9  10407  axdc3lem2  10433  axdc3lem4  10435  axcclem  10439  zorn2lem7  10484  wunr1om  10701  tskr1om  10749  grothomex  10811  prnmadd  10979  ltaprlem  11026  mulgt0sr  11087  0cnALT2  11436  renegcli  11508  peano2nn  12211  bndndx  12458  uzn0  12826  ublbneg  12904  om2uzrani  13904  uzrdgfni  13910  exprelprel  14437  rtrclreclem3  14994  rtrclind  14999  rexanuz2  15283  caurcvg  15610  caucvg  15612  infcvgaux1i  15790  vdwlem6  16906  dfgrp2e  18835  efgrelexlemb  19602  cygth  21100  psgnghm  21106  iscldtop  22568  opnneiid  22599  pnfnei  22693  mnfnei  22694  discmp  22871  cmpsublem  22872  cmpfi  22881  2ndcredom  22923  2ndc1stc  22924  2ndcdisj  22929  kgenidm  23020  methaus  23998  xrtgioo  24291  caun0  24767  ovolmge0  24963  itg2lcl  25214  aannenlem2  25811  aannenlem3  25812  aaliou2  25822  2lgslem1b  26862  2sqlem2  26888  ostth  27109  nodmon  27120  sltval2  27126  bdayfo  27147  madef  27318  addsprop  27427  negsprop  27476  mulsprop  27553  midwwlks2s3  29173  3cyclfrgrrn1  29505  3cyclfrgrrn  29506  h1de2ctlem  30773  h1de2ci  30774  spansni  30775  spanunsni  30797  riesz3i  31280  adjbd1o  31303  rnbra  31325  pjnmopi  31366  dfpjop  31400  atom1d  31571  cvexchlem  31586  cdj1i  31651  cdj3lem1  31652  hasheuni  33014  cvmlift2lem12  34236  satfrnmapom  34292  sat1el2xp  34301  fmla1  34309  gonar  34317  goalr  34319  fmla0disjsuc  34320  mrsubccat  34440  msrid  34467  elmthm  34498  untint  34612  nnuni  34627  dfon2lem3  34688  dfon2lem7  34692  dfrdg2  34698  finminlem  35108  fneint  35138  ptrecube  36393  poimirlem26  36419  poimirlem27  36420  poimirlem29  36422  poimirlem30  36423  zerdivemp1x  36721  dochsnnz  40227  ismrc  41310  eldiophb  41366  eldioph4b  41420  dfacbasgrp  41721  dfsucon  42145  subsaliuncllem  44946  icoresmbl  45132  elsetpreimafvssdm  45927  sprsymrelfvlem  46031  sprsymrelf1lem  46032  prmdvdsfmtnof1lem2  46126  uspgropssxp  46395  0aryfvalel  47160