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

Theorem rspcdv 3452
 Description: Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1 (𝜑𝐴𝐵)
rspcdv.2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rspcdv (𝜑 → (∀𝑥𝐵 𝜓𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcdv
StepHypRef Expression
1 rspcdv.1 . 2 (𝜑𝐴𝐵)
2 rspcdv.2 . . 3 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
32biimpd 219 . 2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
41, 3rspcimdv 3450 1 (𝜑 → (∀𝑥𝐵 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∀wral 3050 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-v 3342 This theorem is referenced by:  ralxfrd  5028  ralxfrdOLD  5029  ralxfrd2  5033  suppofss1d  7502  suppofss2d  7503  zindd  11690  wrd2ind  13697  ismri2dad  16519  mreexd  16524  mreexexlemd  16526  catcocl  16567  catass  16568  moni  16617  subccocl  16726  funcco  16752  fullfo  16793  fthf1  16798  nati  16836  mrcmndind  17587  idsrngd  19084  uspgr2wlkeq  26773  crctcshwlkn0lem4  26937  crctcshwlkn0lem5  26938  wwlknllvtx  26971  0enwwlksnge1  26994  wlkiswwlks2lem5  27003  clwlkclwwlklem2a  27142  clwlkclwwlklem2  27144  clwwisshclwws  27159  clwwlkinwwlk  27190  umgr2cwwk2dif  27216  rngurd  30118  esumcvg  30478  inelcarsg  30703  carsgclctunlem1  30709  orvcelel  30861  signsply0  30958  onint1  32775  rspcdvinvd  38994  ralbinrald  41723  fargshiftfva  41907  evengpop3  42214  evengpoap3  42215  snlindsntorlem  42787
 Copyright terms: Public domain W3C validator