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