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 ) )