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 ∈ V → ⦋ C / x⦌ A B = ⦋ C / x⦌ A ⦋ C / x⦌ B

Proof

Step Hyp Ref Expression
1 csbun ⊢ ⦋ C / x⦌ A ∪ B = ⦋ C / x⦌ A ∪ ⦋ C / x⦌ B
2 csbsng ⊢ C ∈ V → ⦋ C / x⦌ A = ⦋ C / x⦌ A
3 csbsng ⊢ C ∈ V → ⦋ C / x⦌ B = ⦋ C / x⦌ B
4 2 3 uneq12d ⊢ C ∈ V → ⦋ C / x⦌ A ∪ ⦋ C / x⦌ B = ⦋ C / x⦌ A ∪ ⦋ C / x⦌ B
5 1 4 eqtrid ⊢ C ∈ V → ⦋ C / x⦌ A ∪ B = ⦋ C / x⦌ A ∪ ⦋ C / x⦌ B
6 df-pr ⊢ A B = A ∪ B
7 6 csbeq2i ⊢ ⦋ C / x⦌ A B = ⦋ C / x⦌ A ∪ B
8 df-pr ⊢ ⦋ C / x⦌ A ⦋ C / x⦌ B = ⦋ C / x⦌ A ∪ ⦋ C / x⦌ B
9 5 7 8 3eqtr4g ⊢ C ∈ V → ⦋ C / x⦌ A B = ⦋ C / x⦌ A ⦋ C / x⦌ B