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