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