Metamath Proof Explorer


Theorem csbov123

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

Ref Expression
Assertion csbov123 A/xBFC=A/xBA/xFA/xC

Proof

Step Hyp Ref Expression
1 csbeq1 y=Ay/xBFC=A/xBFC
2 csbeq1 y=Ay/xF=A/xF
3 csbeq1 y=Ay/xB=A/xB
4 csbeq1 y=Ay/xC=A/xC
5 2 3 4 oveq123d y=Ay/xBy/xFy/xC=A/xBA/xFA/xC
6 1 5 eqeq12d y=Ay/xBFC=y/xBy/xFy/xCA/xBFC=A/xBA/xFA/xC
7 vex yV
8 nfcsb1v _xy/xB
9 nfcsb1v _xy/xF
10 nfcsb1v _xy/xC
11 8 9 10 nfov _xy/xBy/xFy/xC
12 csbeq1a x=yF=y/xF
13 csbeq1a x=yB=y/xB
14 csbeq1a x=yC=y/xC
15 12 13 14 oveq123d x=yBFC=y/xBy/xFy/xC
16 7 11 15 csbief y/xBFC=y/xBy/xFy/xC
17 6 16 vtoclg AVA/xBFC=A/xBA/xFA/xC
18 csbprc ¬AVA/xBFC=
19 df-ov A/xBA/xFA/xC=A/xFA/xBA/xC
20 csbprc ¬AVA/xF=
21 20 fveq1d ¬AVA/xFA/xBA/xC=A/xBA/xC
22 0fv A/xBA/xC=
23 21 22 eqtrdi ¬AVA/xFA/xBA/xC=
24 19 23 eqtr2id ¬AV=A/xBA/xFA/xC
25 18 24 eqtrd ¬AVA/xBFC=A/xBA/xFA/xC
26 17 25 pm2.61i A/xBFC=A/xBA/xFA/xC