This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝐵 → ( ∙ ‘ 𝐴 ) = ( ∗ ‘ 𝐴 ) )