This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )