Theorem csbrn

Description: Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012)

	Ref	Expression
Assertion	csbrn	⊢ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step	Hyp	Ref	Expression
1		csbima12	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ V )
2		csbconstg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ V = V )
3	2	imaeq2d	⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ V ) )
4		0ima	⊢ ( ∅ “ V ) = ∅
5	4	eqcomi	⊢ ∅ = ( ∅ “ V )
6		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
7	6	imaeq1d	⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ∅ “ ⦋ 𝐴 / 𝑥 ⦌ V ) )
8		0ima	⊢ ( ∅ “ ⦋ 𝐴 / 𝑥 ⦌ V ) = ∅
9	7 8	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ V ) = ∅ )
10	6	imaeq1d	⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ V ) = ( ∅ “ V ) )
11	5 9 10	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ V ) )
12	3 11	pm2.61i	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ V )
13	1 12	eqtri	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ V )
14		dfrn4	⊢ ran 𝐵 = ( 𝐵 “ V )
15	14	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ V )
16		dfrn4	⊢ ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ V )
17	13 15 16	3eqtr4i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵