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

Theorem rspcdv 3564
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 230 . 2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
41, 3rspcimdv 3562 1 (𝜑 → (∀𝑥𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1525  wcel 2083  wral 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ral 3112  df-v 3442
This theorem is referenced by:  ralxfrd  5207  ralxfrd2  5211  reuop  6026  suppofss1d  7726  suppofss2d  7727  zindd  11937  wrd2ind  13925  ismri2dad  16741  mreexd  16746  mreexexlemd  16748  catcocl  16789  catass  16790  moni  16839  subccocl  16948  funcco  16974  fullfo  17015  fthf1  17020  nati  17058  mndind  17809  idsrngd  19327  uspgr2wlkeq  27114  crctcshwlkn0lem4  27277  crctcshwlkn0lem5  27278  wwlknllvtx  27310  0enwwlksnge1  27328  wlkiswwlks2lem5  27337  clwlkclwwlklem2a  27462  clwlkclwwlklem2  27464  clwwisshclwws  27479  clwwlkinwwlk  27504  umgr2cwwk2dif  27529  wrdt2ind  30302  rngurd  30507  fedgmullem2  30626  esumcvg  30958  inelcarsg  31182  carsgclctunlem1  31188  orvcelel  31340  signsply0  31434  onint1  33408  qsalrel  38676  rspcdvinvd  40031  ralbinrald  42859  fargshiftfva  43107  reupr  43188  evengpop3  43467  evengpoap3  43468  isomgrsym  43505  snlindsntorlem  44027
  Copyright terms: Public domain W3C validator