Metamath Proof Explorer


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 ) )