Metamath Proof Explorer

Theorem dffun6

Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995)

Ref Expression
Assertion dffun6 
|- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ x F
2 nfcv 
 |-  F/_ y F
3 1 2 dffun6f 
 |-  ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )