Theorem elefmndbas2

Description: Two ways of saying a function is a mapping of A to itself. (Contributed by AV, 27-Jan-2024) (Proof shortened by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	efmndbas.g	|- G = ( EndoFMnd ` A )
	efmndbas.b	|- B = ( Base ` G )
Assertion	elefmndbas2	|- ( F e. V -> ( F e. B <-> F : A --> A ) )

Proof

Step	Hyp	Ref	Expression
1		efmndbas.g	|- G = ( EndoFMnd ` A )
2		efmndbas.b	|- B = ( Base ` G )
3	1 2	efmndbasabf	|- B = { f | f : A --> A }
4	3	a1i	|- ( F e. V -> B = { f | f : A --> A } )
5	4	eleq2d	|- ( F e. V -> ( F e. B <-> F e. { f | f : A --> A } ) )
6		feq1	|- ( f = F -> ( f : A --> A <-> F : A --> A ) )
7		eqid	|- { f | f : A --> A } = { f | f : A --> A }
8	6 7	elab2g	|- ( F e. V -> ( F e. { f | f : A --> A } <-> F : A --> A ) )
9	5 8	bitrd	|- ( F e. V -> ( F e. B <-> F : A --> A ) )