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

Metamath Proof Explorer

Theorem csbid

Description: Analogue of sbid for proper substitution into a class. (Contributed by NM, 10-Nov-2005)

		Ref	Expression
	Assertion	csbid	$⊢ ⦋ x / x ⦌ A = A$

Step	Hyp	Ref	Expression
1		df-csb	$⊢ ⦋ x / x ⦌ A = \{y \| \underset{˙}{[} x / x \underset{˙}{]} y \in A\}$
2		sbcid	$⊢ \underset{˙}{[} x / x \underset{˙}{]} y \in A \leftrightarrow y \in A$
3	2	abbii	$⊢ \{y \| \underset{˙}{[} x / x \underset{˙}{]} y \in A\} = \{y \| y \in A\}$
4		abid2	$⊢ \{y \| y \in A\} = A$
5	1 3 4	3eqtri	$⊢ ⦋ x / x ⦌ A = A$