Theorem rexlimiv 3132

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

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

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 3063

This theorem is referenced by:  rexlimdv  3137  rexlimivv  3180  issn  4790  uniss2  4899  disjiun  5088  reuop  6259  ssimaex  6927  ordzsl  7797  onzsl  7798  mpoexw  8032  fsplitfpar  8070  tfrlem8  8325  nneob  8594  ecoptocl  8756  elixpsn  8887  ixpsnf1o  8888  findcard  9100  findcard2  9101  ssfiALT  9110  php  9143  php3  9145  ordunifi  9202  fiint  9239  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  11381  renegcli  11454  peano2nn  12169  bndndx  12412  uzn0  12780  ublbneg  12858  om2uzrani  13887  uzrdgfni  13893  exprelprel  14425  rtrclreclem3  14995  rtrclind  15000  rexanuz2  15285  caurcvg  15612  caucvg  15614  infcvgaux1i  15792  vdwlem6  16926  dfgrp2e  18905  efgrelexlemb  19691  pzriprnglem5  21452  pzriprnglem6  21453  pzriprnglem12  21459  cygth  21538  psgnghm  21547  iscldtop  23051  opnneiid  23082  pnfnei  23176  mnfnei  23177  discmp  23354  cmpsublem  23355  cmpfi  23364  2ndcredom  23406  2ndc1stc  23407  2ndcdisj  23412  kgenidm  23503  methaus  24476  xrtgioo  24763  caun0  25249  ovolmge0  25446  itg2lcl  25696  aannenlem2  26305  aannenlem3  26306  aaliou2  26316  2lgslem1b  27371  2sqlem2  27397  ostth  27618  nodmon  27630  ltsval2  27636  bdayfo  27657  madef  27844  addsprop  27984  negsprop  28043  mulsprop  28138  elons2  28266  nnsge1  28351  onsfi  28364  dfnns2  28380  n0seo  28429  bdaypw2n0bnd  28472  remulscllem1  28508  midwwlks2s3  30037  3cyclfrgrrn1  30372  3cyclfrgrrn  30373  h1de2ctlem  31642  h1de2ci  31643  spansni  31644  spanunsni  31666  riesz3i  32149  adjbd1o  32172  rnbra  32194  pjnmopi  32235  dfpjop  32269  atom1d  32440  cvexchlem  32455  cdj1i  32520  cdj3lem1  32521  hasheuni  34262  cvmlift2lem12  35527  satfrnmapom  35583  sat1el2xp  35592  fmla1  35600  gonar  35608  goalr  35610  fmla0disjsuc  35611  mrsubccat  35731  msrid  35758  elmthm  35789  untint  35925  nnuni  35940  dfon2lem3  35996  dfon2lem7  36000  dfrdg2  36006  finminlem  36531  fneint  36561  ptrecube  37868  poimirlem26  37894  poimirlem27  37895  poimirlem29  37897  poimirlem30  37898  zerdivemp1x  38195  dochsnnz  41823  ismrc  43055  eldiophb  43111  eldioph4b  43165  dfacbasgrp  43462  dfsucon  43876  orbitcl  45310  subsaliuncllem  46712  icoresmbl  46898  elsetpreimafvssdm  47743  sprsymrelfvlem  47847  sprsymrelf1lem  47848  prmdvdsfmtnof1lem2  47942  isgrtri  48300  stgredgel  48314  stgr1  48318  uspgropssxp  48501  0aryfvalel  48991