Theorem nfcsbw

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 12-Oct-2016) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nfcsbw.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfcsbw.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-csb	$$⊢⦋A/y⦌B=\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in B\right\}$$
4		nftru	$$⊢Ⅎz\top$$
5		nftru	$$⊢Ⅎy\top$$
6	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
7	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xB$$
8	7	nfcrd	$$⊢\top \to Ⅎxz\in B$$
9	5 6 8	nfsbcdw	$$⊢\top \to Ⅎx\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in B$$
10	4 9	nfabdw	$$⊢\top \to \underset{\_}{Ⅎ}x\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in B\right\}$$
11	3 10	nfcxfrd	$$⊢\top \to \underset{\_}{Ⅎ}x⦋A/y⦌B$$
12	11	mptru	$$⊢\underset{\_}{Ⅎ}x⦋A/y⦌B$$