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

Theorem rspcdva 3305
 Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
Hypotheses
Ref Expression
rspcdva.1 (𝑥 = 𝐶 → (𝜓𝜒))
rspcdva.2 (𝜑 → ∀𝑥𝐴 𝜓)
rspcdva.3 (𝜑𝐶𝐴)
Assertion
Ref Expression
rspcdva (𝜑𝜒)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜒,𝑥   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcdva
StepHypRef Expression
1 rspcdva.2 . 2 (𝜑 → ∀𝑥𝐴 𝜓)
2 rspcdva.3 . . 3 (𝜑𝐶𝐴)
3 rspcdva.1 . . . 4 (𝑥 = 𝐶 → (𝜓𝜒))
43adantl 482 . . 3 ((𝜑𝑥 = 𝐶) → (𝜓𝜒))
52, 4rspcdv 3302 . 2 (𝜑 → (∀𝑥𝐴 𝜓𝜒))
61, 5mpd 15 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1987  ∀wral 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-v 3192 This theorem is referenced by:  grprinvlem  6837  grprinvd  6838  fin1ai  9075  prmreclem5  15567  gsumzaddlem  18261  ablfac1eu  18412  evlslem1  19455  mdetunilem1  20358  cmpcov  21132  cuspcvg  22045  tayl0  24054  lgamcvglem  24700  wlkonl1iedg  26464  wlkp1lem7  26479  wlkp1lem8  26480  crctcshwlkn0lem6  26610  eupth2eucrct  26977  inelpisys  30040  unelldsys  30044  ldgenpisyslem1  30049  unblimceq0lem  32192  unblimceq0  32193  unbdqndv2  32197  saldifcl  39876
 Copyright terms: Public domain W3C validator