Theorem dffun8

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. Compare dffun7 . (Contributed by NM, 4-Nov-2002) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	dffun8	|- ( Fun A <-> ( Rel A /\ A. x e. dom A E! y x A y ) )

Proof

Step	Hyp	Ref	Expression
1		dffun7	|- ( Fun A <-> ( Rel A /\ A. x e. dom A E* y x A y ) )
2		moeu	|- ( E* y x A y <-> ( E. y x A y -> E! y x A y ) )
3		vex	|- x e. _V
4	3	eldm	|- ( x e. dom A <-> E. y x A y )
5		pm5.5	|- ( E. y x A y -> ( ( E. y x A y -> E! y x A y ) <-> E! y x A y ) )
6	4 5	sylbi	|- ( x e. dom A -> ( ( E. y x A y -> E! y x A y ) <-> E! y x A y ) )
7	2 6	bitrid	|- ( x e. dom A -> ( E* y x A y <-> E! y x A y ) )
8	7	ralbiia	|- ( A. x e. dom A E* y x A y <-> A. x e. dom A E! y x A y )
9	8	anbi2i	|- ( ( Rel A /\ A. x e. dom A E* y x A y ) <-> ( Rel A /\ A. x e. dom A E! y x A y ) )
10	1 9	bitri	|- ( Fun A <-> ( Rel A /\ A. x e. dom A E! y x A y ) )