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

Theorem rspceaimv 3627
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 3177 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3621 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1539  wcel 2107  wral 3060  wrex 3069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070
This theorem is referenced by:  brimralrspcev  5203  rexanre  15386  rexico  15393  rlim2lt  15534  rlim3  15535  rlimconst  15581  rlimcn3  15627  reccn2  15634  cn1lem  15635  o1rlimmul  15656  caucvgrlem  15710  divrcnv  15889  chfacffsupp  22863  chfacfscmulfsupp  22866  chfacfpmmulfsupp  22870  tsmsgsum  24148  tsmsres  24153  tsmsxp  24164  metcnpi3  24560  nrginvrcnlem  24713  nghmcn  24767  metdscn  24879  elcncf1di  24922  volcn  25642  itg2cnlem2  25798  abelthlem8  26484  divlogrlim  26678  cxplim  27016  cxploglim  27022  ftalem1  27117  ftalem2  27118  dchrisum0  27565  nmcvcn  30715  blocni  30825  0cnop  31999  0cnfn  32000  idcnop  32001  lnconi  32053  qqhcn  33993  dnicn  36494  ftc1anc  37709  limsupre3uzlem  45755  fourierdlem87  46213
  Copyright terms: Public domain W3C validator