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

Theorem spv 2038
 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 207 . 2
32spimv 2036 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184  wal 1403 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-12 1878  ax-13 2026 This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638 This theorem is referenced by:  ru  3276  nalset  4531  isowe2  6229  tfisi  6676  findcard2  7794  marypha1lem  7927  setind  8197  karden  8345  kmlem4  8565  axgroth3  9239  ramcl  14756  alexsubALTlem3  20841  i1fd  22380  dfpo2  29968  dfon2lem6  30007  trer  30544  axc11n-16  31961
 Copyright terms: Public domain W3C validator