Metamath Proof Explorer


Theorem dffunsALTV5

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

Ref Expression
Assertion dffunsALTV5 FunsALTV = f Rels | x ran f y ran f x = y x f -1 y f -1 =

Proof

Step Hyp Ref Expression
1 dffunsALTV4 FunsALTV = f Rels | u * x u f x
2 ineccnvmo2 x ran f y ran f x = y x f -1 y f -1 = u * x u f x
3 2 rabbii f Rels | x ran f y ran f x = y x f -1 y f -1 = = f Rels | u * x u f x
4 1 3 eqtr4i FunsALTV = f Rels | x ran f y ran f x = y x f -1 y f -1 =