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 ∈ A ∧ C ∈ 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 ∈ A → B I ↾ A x ↔ B = x ↔ B ∈ A → B I ↾ A C ↔ B = C
5 vex ⊢ x ∈ V
6 5 opres ⊢ B ∈ A → B x ∈ I ↾ A ↔ B x ∈ I
7 df-br ⊢ B I ↾ A x ↔ B x ∈ I ↾ A
8 5 ideq ⊢ B I x ↔ B = x
9 df-br ⊢ B I x ↔ B x ∈ I
10 8 9 bitr3i ⊢ B = x ↔ B x ∈ I
11 6 7 10 3bitr4g ⊢ B ∈ A → B I ↾ A x ↔ B = x
12 4 11 vtoclg ⊢ C ∈ A → B ∈ A → B I ↾ A C ↔ B = C
13 12 impcom ⊢ B ∈ A ∧ C ∈ A → B I ↾ A C ↔ B = C