Metamath Proof Explorer


Theorem staffn

Description: The functionalization is equal to the original function, if it is a function on the right base set. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses staffval.b B = Base R
staffval.i ˙ = * R
staffval.f ˙ = 𝑟𝑓 R
Assertion staffn ˙ Fn B ˙ = ˙

Proof

Step Hyp Ref Expression
1 staffval.b B = Base R
2 staffval.i ˙ = * R
3 staffval.f ˙ = 𝑟𝑓 R
4 dffn5 ˙ Fn B ˙ = x B ˙ x
5 4 biimpi ˙ Fn B ˙ = x B ˙ x
6 1 2 3 staffval ˙ = x B ˙ x
7 5 6 syl6reqr ˙ Fn B ˙ = ˙