This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⦋ 𝐴 / 𝑥 ⦌ 𝐵