Metamath Proof Explorer

Theorem elfunsg

Description: Closed form of elfuns . (Contributed by Scott Fenton, 2-May-2014)

Ref Expression
Assertion elfunsg 
|- ( F e. V -> ( F e. Funs <-> Fun F ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( f = F -> ( f e. Funs <-> F e. Funs ) )
2 funeq 
 |-  ( f = F -> ( Fun f <-> Fun F ) )
3 vex 
 |-  f e. _V
4 3 elfuns 
 |-  ( f e. Funs <-> Fun f )
5 1 2 4 vtoclbg 
 |-  ( F e. V -> ( F e. Funs <-> Fun F ) )