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 ( 𝐶 ∈ 𝑉 → ⦋ 𝐶 / 𝑥 ⦌ { 𝐴 , 𝐵 } = { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 , ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } )

Proof

Step Hyp Ref Expression
1 csbun ⊢ ⦋ 𝐶 / 𝑥 ⦌ ( { 𝐴 } ∪ { 𝐵 } ) = ( ⦋ 𝐶 / 𝑥 ⦌ { 𝐴 } ∪ ⦋ 𝐶 / 𝑥 ⦌ { 𝐵 } )
2 csbsng ⊢ ( 𝐶 ∈ 𝑉 → ⦋ 𝐶 / 𝑥 ⦌ { 𝐴 } = { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 } )
3 csbsng ⊢ ( 𝐶 ∈ 𝑉 → ⦋ 𝐶 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } )
4 2 3 uneq12d ⊢ ( 𝐶 ∈ 𝑉 → ( ⦋ 𝐶 / 𝑥 ⦌ { 𝐴 } ∪ ⦋ 𝐶 / 𝑥 ⦌ { 𝐵 } ) = ( { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 } ∪ { ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } ) )
5 1 4 eqtrid ⊢ ( 𝐶 ∈ 𝑉 → ⦋ 𝐶 / 𝑥 ⦌ ( { 𝐴 } ∪ { 𝐵 } ) = ( { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 } ∪ { ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } ) )
6 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
7 6 csbeq2i ⊢ ⦋ 𝐶 / 𝑥 ⦌ { 𝐴 , 𝐵 } = ⦋ 𝐶 / 𝑥 ⦌ ( { 𝐴 } ∪ { 𝐵 } )
8 df-pr ⊢ { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 , ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } = ( { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 } ∪ { ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } )
9 5 7 8 3eqtr4g ⊢ ( 𝐶 ∈ 𝑉 → ⦋ 𝐶 / 𝑥 ⦌ { 𝐴 , 𝐵 } = { ⦋ 𝐶 / 𝑥 ⦌ 𝐴 , ⦋ 𝐶 / 𝑥 ⦌ 𝐵 } )