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 ( 𝐹𝑉 → ( 𝐹 ∈ FunsALTV ↔ FunALTV 𝐹 ) )

Proof

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