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 ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∪ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

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