Theorem csbgfi

Description: Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019)

	Ref	Expression
Hypotheses	csbgfi.1	$$⊢A\in \mathrm{V}$$
	csbgfi.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	csbgfi	$$⊢⦋A/x⦌B=B$$

Proof

Step	Hyp	Ref	Expression
1		csbgfi.1	$$⊢A\in \mathrm{V}$$
2		csbgfi.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
4	3	eqabri	$$⊢y\in ⦋A/x⦌B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B$$
5	2	nfcri	$$⊢Ⅎxy\in B$$
6	1 5	sbcgfi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in B$$
7	4 6	bitri	$$⊢y\in ⦋A/x⦌B\leftrightarrow y\in B$$
8	7	eqriv	$$⊢⦋A/x⦌B=B$$