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