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 ⊢ B = Base R
staffval.i ⊢ ∗ ˙ = * R
staffval.f ⊢ ∙ ˙ = ∗ 𝑟𝑓 ⁡ R
Assertion stafval ⊢ A ∈ B → ∙ ˙ ⁡ A = ∗ ˙ ⁡ A

Proof

Step Hyp Ref Expression
1 staffval.b ⊢ B = Base R
2 staffval.i ⊢ ∗ ˙ = * R
3 staffval.f ⊢ ∙ ˙ = ∗ 𝑟𝑓 ⁡ R
4 fveq2 ⊢ x = A → ∗ ˙ ⁡ x = ∗ ˙ ⁡ A
5 1 2 3 staffval ⊢ ∙ ˙ = x ∈ B ⟼ ∗ ˙ ⁡ x
6 fvex ⊢ ∗ ˙ ⁡ A ∈ V
7 4 5 6 fvmpt ⊢ A ∈ B → ∙ ˙ ⁡ A = ∗ ˙ ⁡ A