This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbcog

Description: Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020)

Ref Expression
Assertion csbcog ⊢ A ∈ V → ⦋ A / x⦌ B ∘ C = ⦋ A / x⦌ B ∘ ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ y = A → ⦋ y / x⦌ B ∘ C = ⦋ A / x⦌ B ∘ C
2 csbeq1 ⊢ y = A → ⦋ y / x⦌ B = ⦋ A / x⦌ B
3 csbeq1 ⊢ y = A → ⦋ y / x⦌ C = ⦋ A / x⦌ C
4 2 3 coeq12d ⊢ y = A → ⦋ y / x⦌ B ∘ ⦋ y / x⦌ C = ⦋ A / x⦌ B ∘ ⦋ A / x⦌ C
5 1 4 eqeq12d ⊢ y = A → ⦋ y / x⦌ B ∘ C = ⦋ y / x⦌ B ∘ ⦋ y / x⦌ C ↔ ⦋ A / x⦌ B ∘ C = ⦋ A / x⦌ B ∘ ⦋ A / x⦌ C
6 vex ⊢ y ∈ V
7 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
8 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
9 7 8 nfco ⊢ Ⅎ _ x ⦋ y / x⦌ B ∘ ⦋ y / x⦌ C
10 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
11 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
12 10 11 coeq12d ⊢ x = y → B ∘ C = ⦋ y / x⦌ B ∘ ⦋ y / x⦌ C
13 6 9 12 csbief ⊢ ⦋ y / x⦌ B ∘ C = ⦋ y / x⦌ B ∘ ⦋ y / x⦌ C
14 5 13 vtoclg ⊢ A ∈ V → ⦋ A / x⦌ B ∘ C = ⦋ A / x⦌ B ∘ ⦋ A / x⦌ C