Theorem dffunALTV4

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV4 . This is dffun6 . For the X axis and the Y axis you can convert the right side to ( A. x1 E* y1 x1 F y1 /\ Rel F ) . (Contributed by NM, 9-Mar-1995)

	Ref	Expression
Assertion	dffunALTV4	|- ( FunALTV F <-> ( A. u E* x u F x /\ Rel F ) )

Proof

Step	Hyp	Ref	Expression
1		dffunALTV2	|- ( FunALTV F <-> ( ,~ F C_ _I /\ Rel F ) )
2		cossssid4	|- ( ,~ F C_ _I <-> A. u E* x u F x )
3	2	anbi1i	|- ( ( ,~ F C_ _I /\ Rel F ) <-> ( A. u E* x u F x /\ Rel F ) )
4	1 3	bitri	|- ( FunALTV F <-> ( A. u E* x u F x /\ Rel F ) )