Metamath Proof Explorer

Theorem funcnv3

Description: A condition showing a class is single-rooted. (See funcnv ). (Contributed by NM, 26-May-2006)

Ref Expression
Assertion funcnv3 
|- ( Fun `' A <-> A. y e. ran A E! x e. dom A x A y )

Proof

Step Hyp Ref Expression
1 dfrn2 
 |-  ran A = { y | E. x x A y }
2 1 eqabri 
 |-  ( y e. ran A <-> E. x x A y )
3 2 biimpi 
 |-  ( y e. ran A -> E. x x A y )
4 3 biantrurd 
 |-  ( y e. ran A -> ( E* x x A y <-> ( E. x x A y /\ E* x x A y ) ) )
5 4 ralbiia 
 |-  ( A. y e. ran A E* x x A y <-> A. y e. ran A ( E. x x A y /\ E* x x A y ) )
6 funcnv 
 |-  ( Fun `' A <-> A. y e. ran A E* x x A y )
7 df-reu 
 |-  ( E! x e. dom A x A y <-> E! x ( x e. dom A /\ x A y ) )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 breldm 
 |-  ( x A y -> x e. dom A )
11 10 pm4.71ri 
 |-  ( x A y <-> ( x e. dom A /\ x A y ) )
12 11 eubii 
 |-  ( E! x x A y <-> E! x ( x e. dom A /\ x A y ) )
13 df-eu 
 |-  ( E! x x A y <-> ( E. x x A y /\ E* x x A y ) )
14 7 12 13 3bitr2i 
 |-  ( E! x e. dom A x A y <-> ( E. x x A y /\ E* x x A y ) )
15 14 ralbii 
 |-  ( A. y e. ran A E! x e. dom A x A y <-> A. y e. ran A ( E. x x A y /\ E* x x A y ) )
16 5 6 15 3bitr4i 
 |-  ( Fun `' A <-> A. y e. ran A E! x e. dom A x A y )