Metamath Proof Explorer


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 u * x u F x Rel F

Proof

Step Hyp Ref Expression
1 dffunALTV2 FunALTV F F I Rel F
2 cossssid4 F I u * x u F x
3 2 anbi1i F I Rel F u * x u F x Rel F
4 1 3 bitri FunALTV F u * x u F x Rel F