Metamath Proof Explorer


Theorem dffunALTV3

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV3 . Reproduction of dffun2 . For the X axis and the Y axis you can convert the right side to ( A. x1 A. y1 A. y2 ( ( x1 f y1 /\ x1 f y2 ) -> y1 = y2 ) /\ Rel F ) . (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffunALTV3
|- ( FunALTV F <-> ( A. u A. x A. y ( ( u F x /\ u F y ) -> x = y ) /\ Rel F ) )

Proof

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