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 ) )