Metamath Proof Explorer


Theorem elfunsALTV4

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

Ref Expression
Assertion elfunsALTV4 FFunsALTVu*xuFxFRels

Proof

Step Hyp Ref Expression
1 elfunsALTV FFunsALTVFCnvRefRelsFRels
2 cosselcnvrefrels4 FCnvRefRelsu*xuFxFRels
3 cosselrels FRelsFRels
4 3 biantrud FRelsu*xuFxu*xuFxFRels
5 2 4 bitr4id FRelsFCnvRefRelsu*xuFx
6 5 pm5.32ri FCnvRefRelsFRelsu*xuFxFRels
7 1 6 bitri FFunsALTVu*xuFxFRels