Theorem nfcsb

Description: Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfcsbw when possible. (Contributed by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfcsb.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfcsb.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfcsb	$$⊢\underset{\_}{Ⅎ}x⦋A/y⦌B$$

Proof

Step	Hyp	Ref	Expression
1		nfcsb.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfcsb.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		nftru	$$⊢Ⅎy\top$$
4	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
5	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xB$$
6	3 4 5	nfcsbd	$$⊢\top \to \underset{\_}{Ⅎ}x⦋A/y⦌B$$
7	6	mptru	$$⊢\underset{\_}{Ⅎ}x⦋A/y⦌B$$