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 e. _V
	csbgfi.2	|- F/_ x B
Assertion	csbgfi	|- [_ A / x ]_ B = B

Proof

Step	Hyp	Ref	Expression
1		csbgfi.1	|- A e. _V
2		csbgfi.2	|- F/_ x B
3		df-csb	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
4	3	abeq2i	|- ( y e. [_ A / x ]_ B <-> [. A / x ]. y e. B )
5	2	nfcri	|- F/ x y e. B
6	1 5	sbcgfi	|- ( [. A / x ]. y e. B <-> y e. B )
7	4 6	bitri	|- ( y e. [_ A / x ]_ B <-> y e. B )
8	7	eqriv	|- [_ A / x ]_ B = B