Metamath Proof Explorer


Syntax definition wsbc

Description: Extend wff notation to include the proper substitution of a class for a set. Read this notation as "the proper substitution of class A for setvar variable x in wff ph ".

Ref Expression
Assertion wsbc
wff [. A / x ]. ph