Theorem nfcsb1

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

	Ref	Expression
Hypothesis	nfcsb1.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfcsb1	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		nfcsb1.1	$$⊢\underset{\_}{Ⅎ}xA$$
2	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
3	2	nfcsb1d	$$⊢\top \to \underset{\_}{Ⅎ}x⦋A/x⦌B$$
4	3	mptru	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌B$$