Syntax Definition wsbc 2764

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."

Hypotheses

Ref	Expression
wph	wff ph
vx	setvar x
cA	class A

Assertion

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

See definition df-sbc 2765 for more information.