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