Theorem elsymgbas2

Description: Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Mario Carneiro, 28-Jan-2015)

	Ref	Expression
Hypotheses	symgbas.1	|- G = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	elsymgbas2	|- ( F e. V -> ( 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		f1oeq1	|- ( x = F -> ( x : A -1-1-onto-> A <-> F : A -1-1-onto-> A ) )
4	1 2	symgbas	|- B = { x | x : A -1-1-onto-> A }
5	3 4	elab2g	|- ( F e. V -> ( F e. B <-> F : A -1-1-onto-> A ) )