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
|- [_ A / x ]_ ran B = ran [_ A / x ]_ B

Proof

Step Hyp Ref Expression
1 csbima12
 |-  [_ A / x ]_ ( B " _V ) = ( [_ A / x ]_ B " [_ A / x ]_ _V )
2 csbconstg
 |-  ( A e. _V -> [_ A / x ]_ _V = _V )
3 2 imaeq2d
 |-  ( A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( [_ A / x ]_ B " _V ) )
4 0ima
 |-  ( (/) " _V ) = (/)
5 4 eqcomi
 |-  (/) = ( (/) " _V )
6 csbprc
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
7 6 imaeq1d
 |-  ( -. A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( (/) " [_ A / x ]_ _V ) )
8 0ima
 |-  ( (/) " [_ A / x ]_ _V ) = (/)
9 7 8 eqtrdi
 |-  ( -. A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = (/) )
10 6 imaeq1d
 |-  ( -. A e. _V -> ( [_ A / x ]_ B " _V ) = ( (/) " _V ) )
11 5 9 10 3eqtr4a
 |-  ( -. A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( [_ A / x ]_ B " _V ) )
12 3 11 pm2.61i
 |-  ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( [_ A / x ]_ B " _V )
13 1 12 eqtri
 |-  [_ A / x ]_ ( B " _V ) = ( [_ A / x ]_ B " _V )
14 dfrn4
 |-  ran B = ( B " _V )
15 14 csbeq2i
 |-  [_ A / x ]_ ran B = [_ A / x ]_ ( B " _V )
16 dfrn4
 |-  ran [_ A / x ]_ B = ( [_ A / x ]_ B " _V )
17 13 15 16 3eqtr4i
 |-  [_ A / x ]_ ran B = ran [_ A / x ]_ B