Metamath Proof Explorer

Theorem resieq

Description: A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004)

Ref Expression
Assertion resieq 
|- ( ( B e. A /\ C e. A ) -> ( B ( _I |` A ) C <-> B = C ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = C -> ( B ( _I |` A ) x <-> B ( _I |` A ) C ) )
2 eqeq2 
 |-  ( x = C -> ( B = x <-> B = C ) )
3 1 2 bibi12d 
 |-  ( x = C -> ( ( B ( _I |` A ) x <-> B = x ) <-> ( B ( _I |` A ) C <-> B = C ) ) )
4 3 imbi2d 
 |-  ( x = C -> ( ( B e. A -> ( B ( _I |` A ) x <-> B = x ) ) <-> ( B e. A -> ( B ( _I |` A ) C <-> B = C ) ) ) )
5 vex 
 |-  x e. _V
6 5 opres 
 |-  ( B e. A -> ( <. B , x >. e. ( _I |` A ) <-> <. B , x >. e. _I ) )
7 df-br 
 |-  ( B ( _I |` A ) x <-> <. B , x >. e. ( _I |` A ) )
8 5 ideq 
 |-  ( B _I x <-> B = x )
9 df-br 
 |-  ( B _I x <-> <. B , x >. e. _I )
10 8 9 bitr3i 
 |-  ( B = x <-> <. B , x >. e. _I )
11 6 7 10 3bitr4g 
 |-  ( B e. A -> ( B ( _I |` A ) x <-> B = x ) )
12 4 11 vtoclg 
 |-  ( C e. A -> ( B e. A -> ( B ( _I |` A ) C <-> B = C ) ) )
13 12 impcom 
 |-  ( ( B e. A /\ C e. A ) -> ( B ( _I |` A ) C <-> B = C ) )