Metamath Proof Explorer

Theorem brimageg

Description: Closed form of brimage . (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion brimageg 
|- ( ( A e. V /\ B e. W ) -> ( A Image R B <-> B = ( R " A ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = A -> ( x Image R y <-> A Image R y ) )
2 imaeq2 
 |-  ( x = A -> ( R " x ) = ( R " A ) )
3 2 eqeq2d 
 |-  ( x = A -> ( y = ( R " x ) <-> y = ( R " A ) ) )
4 1 3 bibi12d 
 |-  ( x = A -> ( ( x Image R y <-> y = ( R " x ) ) <-> ( A Image R y <-> y = ( R " A ) ) ) )
5 breq2 
 |-  ( y = B -> ( A Image R y <-> A Image R B ) )
6 eqeq1 
 |-  ( y = B -> ( y = ( R " A ) <-> B = ( R " A ) ) )
7 5 6 bibi12d 
 |-  ( y = B -> ( ( A Image R y <-> y = ( R " A ) ) <-> ( A Image R B <-> B = ( R " A ) ) ) )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 brimage 
 |-  ( x Image R y <-> y = ( R " x ) )
11 4 7 10 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( A Image R B <-> B = ( R " A ) ) )