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

Hypotheses

Ref	Expression
wph	wff ph
vx	set x
cA	class A

Assertion

Ref	Expression
wsbc	wff [A / x]ph

See definition df-sbc 1441 for more information.

metamath.org