Theorem elfunsALTVfunALTV

Description: The element of the class of functions and the function predicate are the same when F is a set. (Contributed by Peter Mazsa, 26-Jul-2021)

	Ref	Expression
Assertion	elfunsALTVfunALTV	|- ( F e. V -> ( F e. FunsALTV <-> FunALTV F ) )

Proof

Step	Hyp	Ref	Expression
1		cossex	|- ( F e. V -> ,~ F e. _V )
2		elcnvrefrelsrel	|- ( ,~ F e. _V -> ( ,~ F e. CnvRefRels <-> CnvRefRel ,~ F ) )
3	1 2	syl	|- ( F e. V -> ( ,~ F e. CnvRefRels <-> CnvRefRel ,~ F ) )
4		elrelsrel	|- ( F e. V -> ( F e. Rels <-> Rel F ) )
5	3 4	anbi12d	|- ( F e. V -> ( ( ,~ F e. CnvRefRels /\ F e. Rels ) <-> ( CnvRefRel ,~ F /\ Rel F ) ) )
6		elfunsALTV	|- ( F e. FunsALTV <-> ( ,~ F e. CnvRefRels /\ F e. Rels ) )
7		df-funALTV	|- ( FunALTV F <-> ( CnvRefRel ,~ F /\ Rel F ) )
8	5 6 7	3bitr4g	|- ( F e. V -> ( F e. FunsALTV <-> FunALTV F ) )