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

Theorem rspceaimv 3614
 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 345 . . 3 (𝑥 = 𝐴 → ((𝜑𝜒) ↔ (𝜓𝜒)))
32ralbidv 3192 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3609 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115  ∀wral 3133  ∃wrex 3134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-ral 3138  df-rex 3139 This theorem is referenced by:  brimralrspcev  5113  rexanre  14706  rexico  14713  rlim2lt  14854  rlim3  14855  rlimconst  14901  rlimcn2  14947  reccn2  14953  cn1lem  14954  o1rlimmul  14975  caucvgrlem  15029  divrcnv  15207  chfacffsupp  21464  chfacfscmulfsupp  21467  chfacfpmmulfsupp  21471  tsmsgsum  22747  tsmsres  22752  tsmsxp  22763  metcnpi3  23156  nrginvrcnlem  23300  nghmcn  23354  metdscn  23464  elcncf1di  23503  volcn  24213  itg2cnlem2  24369  abelthlem8  25037  divlogrlim  25229  cxplim  25560  cxploglim  25566  ftalem1  25661  ftalem2  25662  dchrisum0  26107  nmcvcn  28481  blocni  28591  0cnop  29765  0cnfn  29766  idcnop  29767  lnconi  29819  qqhcn  31289  dnicn  33888  ftc1anc  35083  limsupre3uzlem  42303  fourierdlem87  42761
 Copyright terms: Public domain W3C validator