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

Metamath Proof Explorer

Theorem csbun

Description: Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015) (Revised by Mario Carneiro, 11-Dec-2016) (Revised by NM, 13-Sep-2018)

Ref Expression
Assertion csbun ⊢ ⦋ A / x⦌ B ∪ C = ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ y = A → ⦋ y / x⦌ B ∪ C = ⦋ A / x⦌ B ∪ C
2 csbeq1 ⊢ y = A → ⦋ y / x⦌ B = ⦋ A / x⦌ B
3 csbeq1 ⊢ y = A → ⦋ y / x⦌ C = ⦋ A / x⦌ C
4 2 3 uneq12d ⊢ y = A → ⦋ y / x⦌ B ∪ ⦋ y / x⦌ C = ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C
5 1 4 eqeq12d ⊢ y = A → ⦋ y / x⦌ B ∪ C = ⦋ y / x⦌ B ∪ ⦋ y / x⦌ C ↔ ⦋ A / x⦌ B ∪ C = ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C
6 vex ⊢ y ∈ V
7 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
8 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
9 7 8 nfun ⊢ Ⅎ _ x ⦋ y / x⦌ B ∪ ⦋ y / x⦌ C
10 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
11 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
12 10 11 uneq12d ⊢ x = y → B ∪ C = ⦋ y / x⦌ B ∪ ⦋ y / x⦌ C
13 6 9 12 csbief ⊢ ⦋ y / x⦌ B ∪ C = ⦋ y / x⦌ B ∪ ⦋ y / x⦌ C
14 5 13 vtoclg ⊢ A ∈ V → ⦋ A / x⦌ B ∪ C = ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C
15 un0 ⊢ ∅ ∪ ∅ = ∅
16 15 a1i ⊢ ¬ A ∈ V → ∅ ∪ ∅ = ∅
17 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ B = ∅
18 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ C = ∅
19 17 18 uneq12d ⊢ ¬ A ∈ V → ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C = ∅ ∪ ∅
20 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ B ∪ C = ∅
21 16 19 20 3eqtr4rd ⊢ ¬ A ∈ V → ⦋ A / x⦌ B ∪ C = ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C
22 14 21 pm2.61i ⊢ ⦋ A / x⦌ B ∪ C = ⦋ A / x⦌ B ∪ ⦋ A / x⦌ C