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

Metamath Proof Explorer

Theorem csbprg

Description: Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018)

Ref Expression
Assertion csbprg 
|- ( C e. V -> [_ C / x ]_ { A , B } = { [_ C / x ]_ A , [_ C / x ]_ B } )

Proof

Step Hyp Ref Expression
1 csbun 
 |-  [_ C / x ]_ ( { A } u. { B } ) = ( [_ C / x ]_ { A } u. [_ C / x ]_ { B } )
2 csbsng 
 |-  ( C e. V -> [_ C / x ]_ { A } = { [_ C / x ]_ A } )
3 csbsng 
 |-  ( C e. V -> [_ C / x ]_ { B } = { [_ C / x ]_ B } )
4 2 3 uneq12d 
 |-  ( C e. V -> ( [_ C / x ]_ { A } u. [_ C / x ]_ { B } ) = ( { [_ C / x ]_ A } u. { [_ C / x ]_ B } ) )
5 1 4 eqtrid 
 |-  ( C e. V -> [_ C / x ]_ ( { A } u. { B } ) = ( { [_ C / x ]_ A } u. { [_ C / x ]_ B } ) )
6 df-pr 
 |-  { A , B } = ( { A } u. { B } )
7 6 csbeq2i 
 |-  [_ C / x ]_ { A , B } = [_ C / x ]_ ( { A } u. { B } )
8 df-pr 
 |-  { [_ C / x ]_ A , [_ C / x ]_ B } = ( { [_ C / x ]_ A } u. { [_ C / x ]_ B } )
9 5 7 8 3eqtr4g 
 |-  ( C e. V -> [_ C / x ]_ { A , B } = { [_ C / x ]_ A , [_ C / x ]_ B } )