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	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		vx	⊢ 𝑥
2		cB	⊢ 𝐵
3	1 0 2	csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵
4		vy	⊢ 𝑦
5	4	cv	⊢ 𝑦
6	5 2	wcel	⊢ 𝑦 ∈ 𝐵
7	6 1 0	wsbc	⊢ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵
8	7 4	cab	⊢ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
9	3 8	wceq	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }