Theorem rexlimiv 3154

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimdv  3159  rexlimivaOLD  3192  rexlimivwOLD  3193  rexlimivv  3207  issn  4857  uniss2  4965  disjiun  5154  reuop  6324  ssimaex  7007  ordzsl  7882  onzsl  7883  mpoexw  8119  fsplitfpar  8159  tfrlem8  8440  nneob  8712  ecoptocl  8865  elixpsn  8995  ixpsnf1o  8996  findcard  9229  findcard2  9230  ssfiALT  9241  php  9273  php3  9275  phpOLD  9285  php3OLD  9287  ordunifi  9354  fiint  9394  fiintOLD  9395  en3lp  9683  inf0  9690  inf3lemd  9696  inf3lem6  9702  noinfep  9729  cantnfvalf  9734  dmttrcl  9790  rnttrcl  9791  ttrclselem1  9794  trcl  9797  bndrank  9910  rankc2  9940  tcrank  9953  ficardom  10030  ac10ct  10103  isinfcard  10161  alephfp  10177  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  ackbij2  10311  fin23lem16  10404  fin23lem29  10410  fin17  10463  fin1a2lem6  10474  itunitc  10490  hsmexlem9  10494  axdc3lem2  10520  axdc3lem4  10522  axcclem  10526  zorn2lem7  10571  wunr1om  10788  tskr1om  10836  grothomex  10898  prnmadd  11066  ltaprlem  11113  mulgt0sr  11174  0cnALT2  11525  renegcli  11597  peano2nn  12305  bndndx  12552  uzn0  12920  ublbneg  12998  om2uzrani  14003  uzrdgfni  14009  exprelprel  14539  rtrclreclem3  15109  rtrclind  15114  rexanuz2  15398  caurcvg  15725  caucvg  15727  infcvgaux1i  15905  vdwlem6  17033  dfgrp2e  19003  efgrelexlemb  19792  pzriprnglem5  21519  pzriprnglem6  21520  pzriprnglem12  21526  cygth  21613  psgnghm  21621  iscldtop  23124  opnneiid  23155  pnfnei  23249  mnfnei  23250  discmp  23427  cmpsublem  23428  cmpfi  23437  2ndcredom  23479  2ndc1stc  23480  2ndcdisj  23485  kgenidm  23576  methaus  24554  xrtgioo  24847  caun0  25334  ovolmge0  25531  itg2lcl  25782  aannenlem2  26389  aannenlem3  26390  aaliou2  26400  2lgslem1b  27454  2sqlem2  27480  ostth  27701  nodmon  27713  sltval2  27719  bdayfo  27740  madef  27913  addsprop  28027  negsprop  28085  mulsprop  28174  elons2  28299  nnsge1  28364  dfnns2  28380  n0seo  28423  0reno  28447  remulscllem1  28450  midwwlks2s3  29985  3cyclfrgrrn1  30317  3cyclfrgrrn  30318  h1de2ctlem  31587  h1de2ci  31588  spansni  31589  spanunsni  31611  riesz3i  32094  adjbd1o  32117  rnbra  32139  pjnmopi  32180  dfpjop  32214  atom1d  32385  cvexchlem  32400  cdj1i  32465  cdj3lem1  32466  hasheuni  34049  cvmlift2lem12  35282  satfrnmapom  35338  sat1el2xp  35347  fmla1  35355  gonar  35363  goalr  35365  fmla0disjsuc  35366  mrsubccat  35486  msrid  35513  elmthm  35544  untint  35674  nnuni  35689  dfon2lem3  35749  dfon2lem7  35753  dfrdg2  35759  finminlem  36284  fneint  36314  ptrecube  37580  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem30  37610  zerdivemp1x  37907  dochsnnz  41407  ismrc  42657  eldiophb  42713  eldioph4b  42767  dfacbasgrp  43065  dfsucon  43485  subsaliuncllem  46278  icoresmbl  46464  elsetpreimafvssdm  47260  sprsymrelfvlem  47364  sprsymrelf1lem  47365  prmdvdsfmtnof1lem2  47459  isgrtri  47794  uspgropssxp  47867  0aryfvalel  48368