MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspceaimv Structured version   Visualization version   GIF version

Theorem rspceaimv 3557
Description: Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.)
Hypothesis
Ref Expression
rspceaimv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspceaimv ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑥,𝐶   𝜓,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑦)   𝐵(𝑦)   𝐶(𝑦)

Proof of Theorem rspceaimv
StepHypRef Expression
1 rspceaimv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
21imbi1d 341 . . 3 (𝑥 = 𝐴 → ((𝜑𝜒) ↔ (𝜓𝜒)))
32ralbidv 3120 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3552 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1539  wcel 2108  wral 3063  wrex 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069
This theorem is referenced by:  brimralrspcev  5131  rexanre  14986  rexico  14993  rlim2lt  15134  rlim3  15135  rlimconst  15181  rlimcn3  15227  reccn2  15234  cn1lem  15235  o1rlimmul  15256  caucvgrlem  15312  divrcnv  15492  chfacffsupp  21913  chfacfscmulfsupp  21916  chfacfpmmulfsupp  21920  tsmsgsum  23198  tsmsres  23203  tsmsxp  23214  metcnpi3  23608  nrginvrcnlem  23761  nghmcn  23815  metdscn  23925  elcncf1di  23964  volcn  24675  itg2cnlem2  24832  abelthlem8  25503  divlogrlim  25695  cxplim  26026  cxploglim  26032  ftalem1  26127  ftalem2  26128  dchrisum0  26573  nmcvcn  28958  blocni  29068  0cnop  30242  0cnfn  30243  idcnop  30244  lnconi  30296  qqhcn  31841  dnicn  34599  ftc1anc  35785  limsupre3uzlem  43166  fourierdlem87  43624
  Copyright terms: Public domain W3C validator