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) (Revised by Gino Giotto, 10-Jan-2024)

	Ref	Expression
Hypotheses	nfcsbw.1	|- F/_ x A
	nfcsbw.2	|- F/_ x B
Assertion	nfcsbw	|- F/_ x [_ A / y ]_ B

Proof

Step	Hyp	Ref	Expression
1		nfcsbw.1	|- F/_ x A
2		nfcsbw.2	|- F/_ x B
3		df-csb	|- [_ A / y ]_ B = { z | [. A / y ]. z e. B }
4		nftru	|- F/ z T.
5		nftru	|- F/ y T.
6	1	a1i	|- ( T. -> F/_ x A )
7	2	a1i	|- ( T. -> F/_ x B )
8	7	nfcrd	|- ( T. -> F/ x z e. B )
9	5 6 8	nfsbcdw	|- ( T. -> F/ x [. A / y ]. z e. B )
10	4 9	nfabdw	|- ( T. -> F/_ x { z | [. A / y ]. z e. B } )
11	3 10	nfcxfrd	|- ( T. -> F/_ x [_ A / y ]_ B )
12	11	mptru	|- F/_ x [_ A / y ]_ B