Theorem rexlimiv 3159

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

Syntax hints:   → wi 4   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexlimdv  3164  rexlimivv  3207  issn  4792  uniss2  4902  disjiun  5092  reuop  6283  ssimaex  6956  ordzsl  7829  onzsl  7830  mpoexw  8063  fsplitfpar  8101  tfrlem8  8359  nneob  8630  ecoptocl  8793  elixpsn  8923  ixpsnf1o  8924  findcard  9136  findcard2  9137  ssfiALT  9146  php  9179  php3  9181  ordunifi  9238  fiint  9274  en3lp  9571  inf0  9578  inf3lemd  9584  inf3lem6  9590  noinfep  9617  cantnfvalf  9622  dmttrcl  9678  rnttrcl  9679  ttrclselem1  9682  trcl  9685  bndrank  9801  rankc2  9831  tcrank  9844  ficardom  9935  ac10ct  10006  isinfcard  10064  alephfp  10080  dfac5lem4  10098  dfac2b  10102  ackbij2  10213  fin23lem16  10307  fin23lem29  10313  fin17  10366  fin1a2lem6  10377  itunitc  10393  hsmexlem9  10397  axdc3lem2  10423  axdc3lem4  10425  axcclem  10429  zorn2lem7  10474  wunr1om  10692  tskr1om  10740  grothomex  10802  prnmadd  10970  ltaprlem  11017  mulgt0sr  11078  0cnALT2  11434  renegcli  11507  peano2nn  12233  bndndx  12491  uzn0  12867  ublbneg  12945  om2uzrani  13976  uzrdgfni  13982  exprelprel  14515  rtrclreclem3  15085  rtrclind  15090  rexanuz2  15389  caurcvg  15716  caucvg  15718  infcvgaux1i  15899  vdwlem6  17034  dfgrp2e  19018  efgrelexlemb  19808  pzriprnglem5  21592  pzriprnglem6  21593  pzriprnglem12  21599  cygth  21678  psgnghm  21687  iscldtop  23209  opnneiid  23240  pnfnei  23334  mnfnei  23335  discmp  23512  cmpsublem  23513  cmpfi  23522  2ndcredom  23564  2ndc1stc  23565  2ndcdisj  23570  kgenidm  23661  methaus  24634  xrtgioo  24921  caun0  25397  ovolmge0  25593  itg2lcl  25843  aannenlem2  26447  aannenlem3  26448  aaliou2  26458  2lgslem1b  27510  2sqlem2  27536  ostth  27757  nodmon  27768  ltsval2  27774  bdayfo  27795  madef  27983  addsprop  28123  negsprop  28182  mulsprop  28277  elons2  28405  nnsge1  28490  onsfi  28503  dfnns2  28519  n0seo  28568  bdaypw2n0bnd  28611  remulscllem1  28647  midwwlks2s3  30206  3cyclfrgrrn1  30541  3cyclfrgrrn  30542  h1de2ctlem  31812  h1de2ci  31813  spansni  31814  spanunsni  31836  riesz3i  32319  adjbd1o  32342  rnbra  32364  pjnmopi  32405  dfpjop  32439  atom1d  32610  cvexchlem  32625  cdj1i  32690  cdj3lem1  32691  hasheuni  34387  cvmlift2lem12  35672  satfrnmapom  35728  sat1el2xp  35737  fmla1  35745  gonar  35753  goalr  35755  fmla0disjsuc  35756  mrsubccat  35876  msrid  35903  elmthm  35934  untint  36070  nnuni  36085  dfon2lem3  36141  dfon2lem7  36145  dfrdg2  36151  finminlem  36686  fneint  36716  ptrecube  38126  poimirlem26  38152  poimirlem27  38153  poimirlem29  38155  poimirlem30  38156  zerdivemp1x  38453  dochsnnz  42081  ismrc  43289  eldiophb  43345  eldioph4b  43395  dfacbasgrp  43692  dfsucon  44106  orbitcl  45525  subsaliuncllem  46930  icoresmbl  47116  elsetpreimafvssdm  47991  sprsymrelfvlem  48095  sprsymrelf1lem  48096  prmdvdsfmtnof1lem2  48193  isgrtri  48564  stgredgel  48578  stgr1  48582  uspgropssxp  48765  0aryfvalel  49266