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 
|- [_ 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