Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  spv Structured version   Unicode version

Theorem spv 1966
 Description: Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
spv.1
Assertion
Ref Expression
spv
Distinct variable group:   ,
Allowed substitution hints:   (,)   ()

Proof of Theorem spv
StepHypRef Expression
1 spv.1 . . 3
21biimpd 200 . 2
32spimv 1964 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178  wal 1550 This theorem is referenced by:  chvarvOLD  1971  ax10-16  2269  ru  3162  nalset  4343  tfisi  4841  isowe2  6073  findcard2  7351  marypha1lem  7441  setind  7676  karden  7824  kmlem4  8038  axgroth3  8711  ramcl  13402  alexsubALTlem3  18085  i1fd  19576  dfpo2  25383  dfon2lem6  25420  trer  26333 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762  ax-12 1951 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
 Copyright terms: Public domain W3C validator