Metamath Proof Explorer


Theorem elfunsALTV

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

Ref Expression
Assertion elfunsALTV
|- ( F e. FunsALTV <-> ( ,~ F e. CnvRefRels /\ F e. Rels ) )

Proof

Step Hyp Ref Expression
1 dffunsALTV
 |-  FunsALTV = { x e. Rels | ,~ x e. CnvRefRels }
2 cosseq
 |-  ( x = F -> ,~ x = ,~ F )
3 2 eleq1d
 |-  ( x = F -> ( ,~ x e. CnvRefRels <-> ,~ F e. CnvRefRels ) )
4 1 3 rabeqel
 |-  ( F e. FunsALTV <-> ( ,~ F e. CnvRefRels /\ F e. Rels ) )