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

Metamath Proof Explorer

Theorem csb2

Description: Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A . (Contributed by NM, 2-Dec-2013)

		Ref	Expression
	Assertion	csb2	$⊢ ⦋ A / x ⦌ B = \{y \| \exists x (x = A \land y \in B)\}$

Proof

Step	Hyp	Ref	Expression
1		df-csb	$⊢ ⦋ A / x ⦌ B = \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\}$
2		sbc5	$⊢ \underset{˙}{[} A / x \underset{˙}{]} y \in B \leftrightarrow \exists x (x = A \land y \in B)$
3	2	abbii	$⊢ \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\} = \{y \| \exists x (x = A \land y \in B)\}$
4	1 3	eqtri	$⊢ ⦋ A / x ⦌ B = \{y \| \exists x (x = A \land y \in B)\}$