Theorem stafval

Description: The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	staffval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	staffval.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
	staffval.f	⊢ ∙ = ( *rf ‘ 𝑅 )
Assertion	stafval	⊢ ( 𝐴 ∈ 𝐵 → ( ∙ ‘ 𝐴 ) = ( ∗ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		staffval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		staffval.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
3		staffval.f	⊢ ∙ = ( *rf ‘ 𝑅 )
4		fveq2	⊢ ( 𝑥 = 𝐴 → ( ∗ ‘ 𝑥 ) = ( ∗ ‘ 𝐴 ) )
5	1 2 3	staffval	⊢ ∙ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )
6		fvex	⊢ ( ∗ ‘ 𝐴 ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝐴 ∈ 𝐵 → ( ∙ ‘ 𝐴 ) = ( ∗ ‘ 𝐴 ) )