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	⊢ 𝐴 ∈ V
	csbgfi.2	⊢ Ⅎ 𝑥 𝐵
Assertion	csbgfi	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵

Proof

Step	Hyp	Ref	Expression
1		csbgfi.1	⊢ 𝐴 ∈ V
2		csbgfi.2	⊢ Ⅎ 𝑥 𝐵
3		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
4	3	abeq2i	⊢ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 )
5	2	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
6	1 5	sbcgfi	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 )
7	4 6	bitri	⊢ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑦 ∈ 𝐵 )
8	7	eqriv	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵