Metamath Proof Explorer

Theorem symgbasmap

Description: A permutation (element of the symmetric group) is a mapping (or set exponentiation) from a set into itself. (Contributed by AV, 30-Mar-2024)

Ref Expression
Hypotheses symgbas.1 G = SymGrp A
symgbas.2 B = Base G
Assertion symgbasmap F B F A A


Step Hyp Ref Expression
1 symgbas.1 G = SymGrp A
2 symgbas.2 B = Base G
3 1 2 symgbasf F B F : A A
4 simpr F B F : A A F : A A
5 dmfex F B F : A A A V
6 5 5 elmapd F B F : A A F A A F : A A
7 4 6 mpbird F B F : A A F A A
8 3 7 mpdan F B F A A