Metamath Proof Explorer


Theorem csbov1g

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

Ref Expression
Assertion csbov1g AVA/xBFC=A/xBFC

Proof

Step Hyp Ref Expression
1 csbov12g AVA/xBFC=A/xBFA/xC
2 csbconstg AVA/xC=C
3 2 oveq2d AVA/xBFA/xC=A/xBFC
4 1 3 eqtrd AVA/xBFC=A/xBFC