Theorem rexlimiv 3156

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rexlimdv  3161  rexlimivv  3204  issn  4792  uniss2  4902  disjiun  5091  reuop  6291  ssimaex  6963  ordzsl  7841  onzsl  7842  mpoexw  8077  fsplitfpar  8115  tfrlem8  8373  nneob  8644  ecoptocl  8807  elixpsn  8944  ixpsnf1o  8945  findcard  9158  findcard2  9159  ssfiALT  9168  php  9201  php3  9203  ordunifi  9260  fiint  9296  en3lp  9593  inf0  9600  inf3lemd  9606  inf3lem6  9612  noinfep  9639  cantnfvalf  9644  dmttrcl  9700  rnttrcl  9701  ttrclselem1  9704  trcl  9707  bndrank  9823  rankc2  9853  tcrank  9866  ficardom  9966  ac10ct  10037  isinfcard  10095  alephfp  10111  dfac5lem4  10129  dfac2b  10133  ackbij2  10244  fin23lem16  10337  fin23lem29  10343  fin17  10396  fin1a2lem6  10407  itunitc  10423  hsmexlem9  10427  axdc3lem2  10453  axdc3lem4  10455  axcclem  10459  zorn2lem7  10504  wunr1om  10728  tskr1om  10776  grothomex  10838  prnmadd  11006  ltaprlem  11053  mulgt0sr  11114  0cnALT2  11470  renegcli  11543  peano2nn  12269  bndndx  12527  uzn0  12904  ublbneg  12982  om2uzrani  14016  uzrdgfni  14022  exprelprel  14555  rtrclreclem3  15133  rtrclind  15138  rexanuz2  15437  caurcvg  15764  caucvg  15766  infcvgaux1i  15946  vdwlem6  17078  dfgrp2e  19087  efgrelexlemb  19877  pzriprnglem5  21698  pzriprnglem6  21699  pzriprnglem12  21705  cygth  21784  psgnghm  21793  iscldtop  23320  opnneiid  23351  pnfnei  23445  mnfnei  23446  discmp  23623  cmpsublem  23624  cmpfi  23633  2ndcredom  23675  2ndc1stc  23676  2ndcdisj  23682  kgenidm  23773  methaus  24746  xrtgioo  25033  caun0  25509  ovolmge0  25705  itg2lcl  25955  aannenlem2  26565  aannenlem3  26566  aaliou2  26576  2lgslem1b  27628  2sqlem2  27654  ostth  27875  nodmon  27886  ltsval2  27892  bdayfo  27913  madef  28101  addsprop  28241  negsprop  28300  mulsprop  28395  elons2  28523  nnsge1  28608  onsfi  28621  dfnns2  28637  n0seo  28686  bdaypw2n0bnd  28729  remulscllem1  28765  midwwlks2s3  30420  3cyclfrgrrn1  30765  3cyclfrgrrn  30766  h1de2ctlem  32036  h1de2ci  32037  spansni  32038  spanunsni  32060  riesz3i  32543  adjbd1o  32566  rnbra  32588  pjnmopi  32629  dfpjop  32663  atom1d  32834  cvexchlem  32849  cdj1i  32914  cdj3lem1  32915  hasheuni  34595  cvmlift2lem12  35893  satfrnmapom  35949  sat1el2xp  35958  fmla1  35966  gonar  35974  goalr  35976  fmla0disjsuc  35977  mrsubccat  36097  msrid  36124  elmthm  36155  untint  36291  nnuni  36306  dfon2lem3  36362  dfon2lem7  36366  dfrdg2  36372  finminlem  36937  fneint  36967  ptrecube  38369  poimirlem26  38395  poimirlem27  38396  poimirlem29  38398  poimirlem30  38399  zerdivemp1x  38697  dochsnnz  42323  ismrc  43546  eldiophb  43602  eldioph4b  43652  dfacbasgrp  43949  dfsucon  44363  orbitcl  45780  subsaliuncllem  47185  icoresmbl  47371  elsetpreimafvssdm  48286  sprsymrelfvlem  48390  sprsymrelf1lem  48391  prmdvdsfmtnof1lem2  48488  isgrtri  48859  stgredgel  48873  stgr1  48877  uspgropssxp  49060  0aryfvalel  49564