Theorem dffunsALTV5

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

	Ref	Expression
Assertion	dffunsALTV5	|- FunsALTV = { f e. Rels | A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) }

Proof

Step	Hyp	Ref	Expression
1		dffunsALTV4	|- FunsALTV = { f e. Rels | A. u E* x u f x }
2		ineccnvmo2	|- ( A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) <-> A. u E* x u f x )
3	2	rabbii	|- { f e. Rels | A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) } = { f e. Rels | A. u E* x u f x }
4	1 3	eqtr4i	|- FunsALTV = { f e. Rels | A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) }