Syntax Definition wsbc 3047

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

Hypotheses

Ref	Expression
wph	wff φ
vx	setvar x
cA	class A

Assertion

Ref	Expression
wsbc	wff [̣A / x]̣φ

See definition df-sbc 3048 for more information.