Metamath Proof Explorer

Theorem elfunsALTV

Description: Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021)

Ref Expression
Assertion elfunsALTV ⊢ F ∈ FunsALTV ↔ ≀ F ∈ CnvRefRels ∧ F ∈ Rels

Proof

Step Hyp Ref Expression
1 dffunsALTV ⊢ FunsALTV = x ∈ Rels | ≀ x ∈ CnvRefRels
2 cosseq ⊢ x = F → ≀ x = ≀ F
3 2 eleq1d ⊢ x = F → ≀ x ∈ CnvRefRels ↔ ≀ F ∈ CnvRefRels
4 1 3 rabeqel ⊢ F ∈ FunsALTV ↔ ≀ F ∈ CnvRefRels ∧ F ∈ Rels