This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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