Syntax Definition wsbc 1440

Description: Extend wff notation to include the proper substitution of a class for a set. This definition "overloads" the previously defined variable substitution wsb 852 (where the first argument is a set variable rather than a class variable). We take care to ensure that this new definition is a conservative extension. Read this notation as "the proper substitution of class A for set variable x in wff φ".

Hypotheses

Ref	Expression
wph	wff φ
vx	set x
cA	class A

Assertion

Ref	Expression
wsbc	wff [A / x]φ

See definition df-sbc 1441 for more information.

metamath.org