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

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

Proof of Theorem spv
StepHypRef Expression
1 spv.1 . . 3
21biimpd 207 . 2
32spimv 2009 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393
This theorem is referenced by:  axc11n-16  2268  ru  3326  nalset  4589  isowe2  6246  tfisi  6693  findcard2  7780  marypha1lem  7913  setind  8186  karden  8334  kmlem4  8554  axgroth3  9230  ramcl  14547  alexsubALTlem3  20549  i1fd  22088  dfpo2  29184  dfon2lem6  29220  trer  30134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator