Metamath Proof Explorer


Theorem csbin

Description: Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion csbin 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 ineq12d 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 nfin _ 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 ineq12d 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 csbprc ¬ A V A / x B C =
16 csbprc ¬ A V A / x B =
17 csbprc ¬ A V A / x C =
18 16 17 ineq12d ¬ A V A / x B A / x C =
19 in0 =
20 18 19 syl6req ¬ A V = A / x B A / x C
21 15 20 eqtrd ¬ 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