This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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