Metamath Proof Explorer


Theorem ofcfval

Description: Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Hypotheses ofcfval.1 φFFnA
ofcfval.2 φAV
ofcfval.3 φCW
ofcfval.6 φxAFx=B
Assertion ofcfval φFfcRC=xABRC

Proof

Step Hyp Ref Expression
1 ofcfval.1 φFFnA
2 ofcfval.2 φAV
3 ofcfval.3 φCW
4 ofcfval.6 φxAFx=B
5 df-ofc fcR=fV,cVxdomffxRc
6 5 a1i φfcR=fV,cVxdomffxRc
7 simprl φf=Fc=Cf=F
8 7 dmeqd φf=Fc=Cdomf=domF
9 7 fveq1d φf=Fc=Cfx=Fx
10 simprr φf=Fc=Cc=C
11 9 10 oveq12d φf=Fc=CfxRc=FxRC
12 8 11 mpteq12dv φf=Fc=CxdomffxRc=xdomFFxRC
13 fnex FFnAAVFV
14 1 2 13 syl2anc φFV
15 3 elexd φCV
16 1 fndmd φdomF=A
17 16 2 eqeltrd φdomFV
18 17 mptexd φxdomFFxRCV
19 6 12 14 15 18 ovmpod φFfcRC=xdomFFxRC
20 16 eleq2d φxdomFxA
21 20 pm5.32i φxdomFφxA
22 21 4 sylbi φxdomFFx=B
23 22 oveq1d φxdomFFxRC=BRC
24 16 23 mpteq12dva φxdomFFxRC=xABRC
25 19 24 eqtrd φFfcRC=xABRC