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 e. V -> [_ A / x ]_ ( B o. C ) = ( [_ A / x ]_ B o. [_ A / x ]_ C ) )

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ ( B o. C ) = [_ A / x ]_ ( B o. 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 o. [_ y / x ]_ C ) = ( [_ A / x ]_ B o. [_ A / x ]_ C ) )
5 1 4 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ ( B o. C ) = ( [_ y / x ]_ B o. [_ y / x ]_ C ) <-> [_ A / x ]_ ( B o. C ) = ( [_ A / x ]_ B o. [_ A / x ]_ C ) ) )
6 vex 
 |-  y e. _V
7 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
9 7 8 nfco 
 |-  F/_ x ( [_ y / x ]_ B o. [_ 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 o. C ) = ( [_ y / x ]_ B o. [_ y / x ]_ C ) )
13 6 9 12 csbief 
 |-  [_ y / x ]_ ( B o. C ) = ( [_ y / x ]_ B o. [_ y / x ]_ C )
14 5 13 vtoclg 
 |-  ( A e. V -> [_ A / x ]_ ( B o. C ) = ( [_ A / x ]_ B o. [_ A / x ]_ C ) )