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