Metamath Proof Explorer


Theorem elfunsALTV2

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

Ref Expression
Assertion elfunsALTV2 F FunsALTV F I F Rels

Proof

Step Hyp Ref Expression
1 elfunsALTV F FunsALTV F CnvRefRels F Rels
2 cosselcnvrefrels2 F CnvRefRels F I F Rels
3 cosselrels F Rels F Rels
4 3 biantrud F Rels F I F I F Rels
5 2 4 bitr4id F Rels F CnvRefRels F I
6 5 pm5.32ri F CnvRefRels F Rels F I F Rels
7 1 6 bitri F FunsALTV F I F Rels