Description: Closed form of elfuns . (Contributed by Scott Fenton, 2-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | elfunsg | ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ Funs ↔ Fun 𝐹 ) ) |
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 𝐹 ) ) |