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

Metamath Proof Explorer

Theorem nfcsb1d

Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016)

		Ref	Expression
	Hypothesis	nfcsb1d.1	$⊢ φ \to \underline{Ⅎ} x A$
	Assertion	nfcsb1d	$⊢ φ \to \underline{Ⅎ} x ⦋ A / x ⦌ B$

Step	Hyp	Ref	Expression
1		nfcsb1d.1	$⊢ φ \to \underline{Ⅎ} x A$
2		df-csb	$⊢ ⦋ A / x ⦌ B = \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\}$
3		nfv	$⊢ Ⅎ y φ$
4	1	nfsbc1d	$⊢ φ \to Ⅎ x \underset{˙}{[} A / x \underset{˙}{]} y \in B$
5	3 4	nfabdw	$⊢ φ \to \underline{Ⅎ} x \{y \| \underset{˙}{[} A / x \underset{˙}{]} y \in B\}$
6	2 5	nfcxfrd	$⊢ φ \to \underline{Ⅎ} x ⦋ A / x ⦌ B$