Metamath Proof Explorer


Theorem elfunsg

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

Ref Expression
Assertion elfunsg ( 𝐹𝑉 → ( 𝐹 Funs ↔ Fun 𝐹 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ( 𝑓 = 𝐹 → ( 𝑓 Funs 𝐹 Funs ) )
2 funeq ( 𝑓 = 𝐹 → ( Fun 𝑓 ↔ Fun 𝐹 ) )
3 vex 𝑓 ∈ V
4 3 elfuns ( 𝑓 Funs ↔ Fun 𝑓 )
5 1 2 4 vtoclbg ( 𝐹𝑉 → ( 𝐹 Funs ↔ Fun 𝐹 ) )