This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾ 𝐴 ) 𝐶 ↔ 𝐵 = 𝐶 ) )