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 e. B }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	\|- A
1		vx	\|- x
2		cB	\|- B
3	1 0 2	csb	\|- [_ A / x ]_ B
4		vy	\|- y
5	4	cv	\|- y
6	5 2	wcel	\|- y e. B
7	6 1 0	wsbc	\|- [. A / x ]. y e. B
8	7 4	cab	\|- { y \| [. A / x ]. y e. B }
9	3 8	wceq	\|- [_ A / x ]_ B = { y \| [. A / x ]. y e. B }