Metamath Proof Explorer

Theorem brrangeg

Description: Closed form of brrange . (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Assertion brrangeg 
|- ( ( A e. V /\ B e. W ) -> ( A Range B <-> B = ran A ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( a = A -> ( a Range b <-> A Range b ) )
2 rneq 
 |-  ( a = A -> ran a = ran A )
3 2 eqeq2d 
 |-  ( a = A -> ( b = ran a <-> b = ran A ) )
4 1 3 bibi12d 
 |-  ( a = A -> ( ( a Range b <-> b = ran a ) <-> ( A Range b <-> b = ran A ) ) )
5 breq2 
 |-  ( b = B -> ( A Range b <-> A Range B ) )
6 eqeq1 
 |-  ( b = B -> ( b = ran A <-> B = ran A ) )
7 5 6 bibi12d 
 |-  ( b = B -> ( ( A Range b <-> b = ran A ) <-> ( A Range B <-> B = ran A ) ) )
8 vex 
 |-  a e. _V
9 vex 
 |-  b e. _V
10 8 9 brrange 
 |-  ( a Range b <-> b = ran a )
11 4 7 10 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( A Range B <-> B = ran A ) )