# Metamath Proof Explorer

## Theorem ofc2

Description: Right operation by a constant. (Contributed by NM, 7-Oct-2014)

Ref Expression
Hypotheses ofc2.1 ${⊢}{\phi }\to {A}\in {V}$
ofc2.2 ${⊢}{\phi }\to {B}\in {W}$
ofc2.3 ${⊢}{\phi }\to {F}Fn{A}$
ofc2.4 ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to {F}\left({X}\right)={C}$
Assertion ofc2 ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to \left({F}{{R}}_{f}\left({A}×\left\{{B}\right\}\right)\right)\left({X}\right)={C}{R}{B}$

### Proof

Step Hyp Ref Expression
1 ofc2.1 ${⊢}{\phi }\to {A}\in {V}$
2 ofc2.2 ${⊢}{\phi }\to {B}\in {W}$
3 ofc2.3 ${⊢}{\phi }\to {F}Fn{A}$
4 ofc2.4 ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to {F}\left({X}\right)={C}$
5 fnconstg ${⊢}{B}\in {W}\to \left({A}×\left\{{B}\right\}\right)Fn{A}$
6 2 5 syl ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right)Fn{A}$
7 inidm ${⊢}{A}\cap {A}={A}$
8 fvconst2g ${⊢}\left({B}\in {W}\wedge {X}\in {A}\right)\to \left({A}×\left\{{B}\right\}\right)\left({X}\right)={B}$
9 2 8 sylan ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to \left({A}×\left\{{B}\right\}\right)\left({X}\right)={B}$
10 3 6 1 1 7 4 9 ofval ${⊢}\left({\phi }\wedge {X}\in {A}\right)\to \left({F}{{R}}_{f}\left({A}×\left\{{B}\right\}\right)\right)\left({X}\right)={C}{R}{B}$