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

Theorem rspceaimv 3612
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 340 . . 3 (𝑥 = 𝐴 → ((𝜑𝜒) ↔ (𝜓𝜒)))
32ralbidv 3167 . 2 (𝑥 = 𝐴 → (∀𝑦𝐶 (𝜑𝜒) ↔ ∀𝑦𝐶 (𝜓𝜒)))
43rspcev 3606 1 ((𝐴𝐵 ∧ ∀𝑦𝐶 (𝜓𝜒)) → ∃𝑥𝐵𝑦𝐶 (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wral 3050  wrex 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060
This theorem is referenced by:  brimralrspcev  5210  rexanre  15329  rexico  15336  rlim2lt  15477  rlim3  15478  rlimconst  15524  rlimcn3  15570  reccn2  15577  cn1lem  15578  o1rlimmul  15599  caucvgrlem  15655  divrcnv  15834  chfacffsupp  22802  chfacfscmulfsupp  22805  chfacfpmmulfsupp  22809  tsmsgsum  24087  tsmsres  24092  tsmsxp  24103  metcnpi3  24499  nrginvrcnlem  24652  nghmcn  24706  metdscn  24816  elcncf1di  24859  volcn  25579  itg2cnlem2  25736  abelthlem8  26421  divlogrlim  26614  cxplim  26949  cxploglim  26955  ftalem1  27050  ftalem2  27051  dchrisum0  27498  nmcvcn  30577  blocni  30687  0cnop  31861  0cnfn  31862  idcnop  31863  lnconi  31915  qqhcn  33720  dnicn  36095  ftc1anc  37302  limsupre3uzlem  45258  fourierdlem87  45716
  Copyright terms: Public domain W3C validator