Metamath Proof Explorer


Theorem csbfv2g

Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005)

Ref Expression
Assertion csbfv2g ( 𝐴𝐶 𝐴 / 𝑥 ( 𝐹𝐵 ) = ( 𝐹 𝐴 / 𝑥 𝐵 ) )

Proof

Step Hyp Ref Expression
1 csbfv12 𝐴 / 𝑥 ( 𝐹𝐵 ) = ( 𝐴 / 𝑥 𝐹 𝐴 / 𝑥 𝐵 )
2 csbconstg ( 𝐴𝐶 𝐴 / 𝑥 𝐹 = 𝐹 )
3 2 fveq1d ( 𝐴𝐶 → ( 𝐴 / 𝑥 𝐹 𝐴 / 𝑥 𝐵 ) = ( 𝐹 𝐴 / 𝑥 𝐵 ) )
4 1 3 eqtrid ( 𝐴𝐶 𝐴 / 𝑥 ( 𝐹𝐵 ) = ( 𝐹 𝐴 / 𝑥 𝐵 ) )