Theorem symgbasf1o

Description: Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	symgbas.1	|- G = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symgbasf1o	|- ( F e. B -> F : A -1-1-onto-> A )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3	1 2	elsymgbas2	|- ( F e. B -> ( F e. B <-> F : A -1-1-onto-> A ) )
4	3	ibi	|- ( F e. B -> F : A -1-1-onto-> A )