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={\mathrm{Base}}_R$$
	staffval.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	staffval.f	$$⊢\underset{\dot{}}{\bullet }={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
Assertion	stafval	$$⊢A\in B\to \underset{\dot{}}{\bullet }\left(A\right)=\underset{\dot{}}{\ast }\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		staffval.b	$$⊢B={\mathrm{Base}}_R$$
2		staffval.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
3		staffval.f	$$⊢\underset{\dot{}}{\bullet }={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
4		fveq2	$$⊢x=A\to \underset{\dot{}}{\ast }\left(x\right)=\underset{\dot{}}{\ast }\left(A\right)$$
5	1 2 3	staffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in B⟼\underset{\dot{}}{\ast }\left(x\right)\right)$$
6		fvex	$$⊢\underset{\dot{}}{\ast }\left(A\right)\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢A\in B\to \underset{\dot{}}{\bullet }\left(A\right)=\underset{\dot{}}{\ast }\left(A\right)$$