MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wsb Structured version   Visualization version   Unicode version
Syntax Definition wsb 1880
Description: Extend wff definition to include proper substitution (read "the wff that results when y is properly substituted for x in wff ph"). (Contributed by NM, 24-Jan-2006.)
Hypotheses
Ref Expression
wph wff ph
vx setvar x
vy setvar y
Assertion
Ref Expression
wsb wff [ y / x ] ph
See definition df-sb 1881 for more information.
Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator