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 ( ( 𝐵𝐴𝐶𝐴 ) → ( 𝐵 ( I ↾ 𝐴 ) 𝐶𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑥 = 𝐶 → ( 𝐵 ( I ↾ 𝐴 ) 𝑥𝐵 ( I ↾ 𝐴 ) 𝐶 ) )
2 eqeq2 ( 𝑥 = 𝐶 → ( 𝐵 = 𝑥𝐵 = 𝐶 ) )
3 1 2 bibi12d ( 𝑥 = 𝐶 → ( ( 𝐵 ( I ↾ 𝐴 ) 𝑥𝐵 = 𝑥 ) ↔ ( 𝐵 ( I ↾ 𝐴 ) 𝐶𝐵 = 𝐶 ) ) )
4 3 imbi2d ( 𝑥 = 𝐶 → ( ( 𝐵𝐴 → ( 𝐵 ( I ↾ 𝐴 ) 𝑥𝐵 = 𝑥 ) ) ↔ ( 𝐵𝐴 → ( 𝐵 ( I ↾ 𝐴 ) 𝐶𝐵 = 𝐶 ) ) ) )
5 vex 𝑥 ∈ V
6 5 opres ( 𝐵𝐴 → ( ⟨ 𝐵 , 𝑥 ⟩ ∈ ( I ↾ 𝐴 ) ↔ ⟨ 𝐵 , 𝑥 ⟩ ∈ I ) )
7 df-br ( 𝐵 ( I ↾ 𝐴 ) 𝑥 ↔ ⟨ 𝐵 , 𝑥 ⟩ ∈ ( I ↾ 𝐴 ) )
8 5 ideq ( 𝐵 I 𝑥𝐵 = 𝑥 )
9 df-br ( 𝐵 I 𝑥 ↔ ⟨ 𝐵 , 𝑥 ⟩ ∈ I )
10 8 9 bitr3i ( 𝐵 = 𝑥 ↔ ⟨ 𝐵 , 𝑥 ⟩ ∈ I )
11 6 7 10 3bitr4g ( 𝐵𝐴 → ( 𝐵 ( I ↾ 𝐴 ) 𝑥𝐵 = 𝑥 ) )
12 4 11 vtoclg ( 𝐶𝐴 → ( 𝐵𝐴 → ( 𝐵 ( I ↾ 𝐴 ) 𝐶𝐵 = 𝐶 ) ) )
13 12 impcom ( ( 𝐵𝐴𝐶𝐴 ) → ( 𝐵 ( I ↾ 𝐴 ) 𝐶𝐵 = 𝐶 ) )