Metamath Proof Explorer

Theorem dffun9

Description: Alternate definition of a function. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

Ref Expression
Assertion dffun9 
|- ( Fun A <-> ( Rel A /\ A. x e. dom A E* y e. ran A 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 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 brelrn 
 |-  ( x A y -> y e. ran A )
5 4 pm4.71ri 
 |-  ( x A y <-> ( y e. ran A /\ x A y ) )
6 5 mobii 
 |-  ( E* y x A y <-> E* y ( y e. ran A /\ x A y ) )
7 df-rmo 
 |-  ( E* y e. ran A x A y <-> E* y ( y e. ran A /\ x A y ) )
8 6 7 bitr4i 
 |-  ( E* y x A y <-> E* y e. ran A x A y )
9 8 ralbii 
 |-  ( A. x e. dom A E* y x A y <-> A. x e. dom A E* y e. ran A x A y )
10 9 anbi2i 
 |-  ( ( Rel A /\ A. x e. dom A E* y x A y ) <-> ( Rel A /\ A. x e. dom A E* y e. ran A x A y ) )
11 1 10 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x e. dom A E* y e. ran A x A y ) )