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 ∈ 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