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

Metamath Proof Explorer

Theorem elfunsg

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

Ref Expression
Assertion elfunsg ⊢ F ∈ V → F ∈ 𝖥𝗎𝗇𝗌 ↔ Fun ⁡ F

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ f = F → f ∈ 𝖥𝗎𝗇𝗌 ↔ F ∈ 𝖥𝗎𝗇𝗌
2 funeq ⊢ f = F → Fun ⁡ f ↔ Fun ⁡ F
3 vex ⊢ f ∈ V
4 3 elfuns ⊢ f ∈ 𝖥𝗎𝗇𝗌 ↔ Fun ⁡ f
5 1 2 4 vtoclbg ⊢ F ∈ V → F ∈ 𝖥𝗎𝗇𝗌 ↔ Fun ⁡ F