Theorem symgfv

Description: The function value of a permutation. (Contributed by AV, 1-Jan-2019)

	Ref	Expression
Hypotheses	symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgfv	$$⊢\left(F\in B\wedge X\in A\right)\to F\left(X\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3	1 2	symgbasf	$$⊢F\in B\to F:A⟶A$$
4	3	ffvelrnda	$$⊢\left(F\in B\wedge X\in A\right)\to F\left(X\right)\in A$$