Metamath Proof Explorer


Definition df-csb

Description: Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc , to prevent ambiguity. Theorem sbcel1g shows an example of how ambiguity could arise if we did not use distinguished brackets. When A is a proper class, this evaluates to the empty set (see csbprc ). Theorem sbccsb recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005)

Ref Expression
Assertion df-csb A / x B = y | [˙A / x]˙ y B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 vx setvar x
2 cB class B
3 1 0 2 csb class A / x B
4 vy setvar y
5 4 cv setvar y
6 5 2 wcel wff y B
7 6 1 0 wsbc wff [˙A / x]˙ y B
8 7 4 cab class y | [˙A / x]˙ y B
9 3 8 wceq wff A / x B = y | [˙A / x]˙ y B