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

Theorem rspceaimv 3586
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 342 . . 3 (𝑥 = 𝐴 → ((𝜑𝜒) ↔ (𝜓𝜒)))
32ralbidv 3175 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3582 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3065  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075
This theorem is referenced by:  brimralrspcev  5167  rexanre  15232  rexico  15239  rlim2lt  15380  rlim3  15381  rlimconst  15427  rlimcn3  15473  reccn2  15480  cn1lem  15481  o1rlimmul  15502  caucvgrlem  15558  divrcnv  15738  chfacffsupp  22208  chfacfscmulfsupp  22211  chfacfpmmulfsupp  22215  tsmsgsum  23493  tsmsres  23498  tsmsxp  23509  metcnpi3  23905  nrginvrcnlem  24058  nghmcn  24112  metdscn  24222  elcncf1di  24261  volcn  24973  itg2cnlem2  25130  abelthlem8  25801  divlogrlim  25993  cxplim  26324  cxploglim  26330  ftalem1  26425  ftalem2  26426  dchrisum0  26871  nmcvcn  29640  blocni  29750  0cnop  30924  0cnfn  30925  idcnop  30926  lnconi  30978  qqhcn  32575  dnicn  34958  ftc1anc  36162  limsupre3uzlem  43983  fourierdlem87  44441
  Copyright terms: Public domain W3C validator