Metamath Proof Explorer


Theorem csbov

Description: Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018)

Ref Expression
Assertion csbov A / x B F C = B A / x F C

Proof

Step Hyp Ref Expression
1 csbov123 A / x B F C = A / x B A / x F A / x C
2 csbconstg A V A / x B = B
3 csbconstg A V A / x C = C
4 2 3 oveq12d A V A / x B A / x F A / x C = B A / x F C
5 0fv B C =
6 df-ov B C = B C
7 0ov A / x B A / x C =
8 5 6 7 3eqtr4ri A / x B A / x C = B C
9 csbprc ¬ A V A / x F =
10 9 oveqd ¬ A V A / x B A / x F A / x C = A / x B A / x C
11 9 oveqd ¬ A V B A / x F C = B C
12 8 10 11 3eqtr4a ¬ A V A / x B A / x F A / x C = B A / x F C
13 4 12 pm2.61i A / x B A / x F A / x C = B A / x F C
14 1 13 eqtri A / x B F C = B A / x F C