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

Theorem rspceaimv 3625
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 343 . . 3 (𝑥 = 𝐴 → ((𝜑𝜒) ↔ (𝜓𝜒)))
32ralbidv 3194 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3620 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3135  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140  df-rex 3141
This theorem is referenced by:  brimralrspcev  5118  rexanre  14694  rexico  14701  rlim2lt  14842  rlim3  14843  rlimconst  14889  rlimcn2  14935  reccn2  14941  cn1lem  14942  o1rlimmul  14963  caucvgrlem  15017  divrcnv  15195  chfacffsupp  21392  chfacfscmulfsupp  21395  chfacfpmmulfsupp  21399  tsmsgsum  22674  tsmsres  22679  tsmsxp  22690  metcnpi3  23083  nrginvrcnlem  23227  nghmcn  23281  metdscn  23391  elcncf1di  23430  volcn  24134  itg2cnlem2  24290  abelthlem8  24954  divlogrlim  25145  cxplim  25476  cxploglim  25482  ftalem1  25577  ftalem2  25578  dchrisum0  26023  nmcvcn  28399  blocni  28509  0cnop  29683  0cnfn  29684  idcnop  29685  lnconi  29737  qqhcn  31131  dnicn  33728  ftc1anc  34856  limsupre3uzlem  41892  fourierdlem87  42355
  Copyright terms: Public domain W3C validator