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 ∈ V → F ∈ FunsALTV ↔ FunALTV F

Proof

Step Hyp Ref Expression
1 cossex ⊢ F ∈ V → ≀ F ∈ V
2 elcnvrefrelsrel ⊢ ≀ F ∈ V → ≀ F ∈ CnvRefRels ↔ CnvRefRel ≀ F
3 1 2 syl ⊢ F ∈ V → ≀ F ∈ CnvRefRels ↔ CnvRefRel ≀ F
4 elrelsrel ⊢ F ∈ V → F ∈ Rels ↔ Rel ⁡ F
5 3 4 anbi12d ⊢ F ∈ V → ≀ F ∈ CnvRefRels ∧ F ∈ Rels ↔ CnvRefRel ≀ F ∧ Rel ⁡ F
6 elfunsALTV ⊢ F ∈ FunsALTV ↔ ≀ F ∈ CnvRefRels ∧ F ∈ Rels
7 df-funALTV ⊢ FunALTV F ↔ CnvRefRel ≀ F ∧ Rel ⁡ F
8 5 6 7 3bitr4g ⊢ F ∈ V → F ∈ FunsALTV ↔ FunALTV F