PE Home bfol.mm Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  PE Home  >  Th. List  >  wff-psub
Syntax Definition wff-psub 714
Description: Extend WFF definition to include proper substitution syntax, '[𝑡 / 𝑥]'.
Hypotheses
Ref Expression
wff-ph wff 𝜑
term-t term 𝑡
objvar-x objvar 𝑥
Assertion
Ref Expression
wff-psub wff [𝑡 / 𝑥]𝜑
See definition df-psub-D6.2 716 for more information.
Colors of variables: wff objvar term class
  Copyright terms: Public domain W3C validator