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 V A / x V = V
3 2 imaeq2d A V A / x B A / x V = A / x B V
4 0ima V =
5 4 eqcomi = V
6 csbprc ¬ A V A / x B =
7 6 imaeq1d ¬ A V A / x B A / x V = A / x V
8 0ima A / x V =
9 7 8 eqtrdi ¬ A V A / x B A / x V =
10 6 imaeq1d ¬ A V A / x B V = V
11 5 9 10 3eqtr4a ¬ A 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