# Metamath Proof Explorer

## Theorem bj-idres

Description: Alternate expression for the restricted identity relation. The advantage of that expression is to expose it as a "bounded" class, being included in the Cartesian square of the restricting class. (Contributed by BJ, 27-Dec-2023)

This is an alternate of idinxpresid (see idinxpres ). See also elrid and elidinxp . (Proof modification is discouraged.)

Ref Expression
Assertion bj-idres ${⊢}{\mathrm{I}↾}_{{A}}=\mathrm{I}\cap \left({A}×{A}\right)$

### Proof

Step Hyp Ref Expression
1 df-res ${⊢}{\mathrm{I}↾}_{{A}}=\mathrm{I}\cap \left({A}×\mathrm{V}\right)$
2 inss1 ${⊢}\mathrm{I}\cap \left({A}×\mathrm{V}\right)\subseteq \mathrm{I}$
3 relinxp ${⊢}\mathrm{Rel}\left(\mathrm{I}\cap \left({A}×\mathrm{V}\right)\right)$
4 elin ${⊢}⟨{x},{y}⟩\in \left(\mathrm{I}\cap \left({A}×\mathrm{V}\right)\right)↔\left(⟨{x},{y}⟩\in \mathrm{I}\wedge ⟨{x},{y}⟩\in \left({A}×\mathrm{V}\right)\right)$
5 bj-opelidb1 ${⊢}⟨{x},{y}⟩\in \mathrm{I}↔\left({x}\in \mathrm{V}\wedge {x}={y}\right)$
6 5 simprbi ${⊢}⟨{x},{y}⟩\in \mathrm{I}\to {x}={y}$
7 opelxp1 ${⊢}⟨{x},{y}⟩\in \left({A}×\mathrm{V}\right)\to {x}\in {A}$
8 simpr ${⊢}\left({x}={y}\wedge {x}\in {A}\right)\to {x}\in {A}$
9 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
10 9 biimpa ${⊢}\left({x}={y}\wedge {x}\in {A}\right)\to {y}\in {A}$
11 8 10 jca ${⊢}\left({x}={y}\wedge {x}\in {A}\right)\to \left({x}\in {A}\wedge {y}\in {A}\right)$
12 6 7 11 syl2an ${⊢}\left(⟨{x},{y}⟩\in \mathrm{I}\wedge ⟨{x},{y}⟩\in \left({A}×\mathrm{V}\right)\right)\to \left({x}\in {A}\wedge {y}\in {A}\right)$
13 4 12 sylbi ${⊢}⟨{x},{y}⟩\in \left(\mathrm{I}\cap \left({A}×\mathrm{V}\right)\right)\to \left({x}\in {A}\wedge {y}\in {A}\right)$
14 opelxpi ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)\to ⟨{x},{y}⟩\in \left({A}×{A}\right)$
15 13 14 syl ${⊢}⟨{x},{y}⟩\in \left(\mathrm{I}\cap \left({A}×\mathrm{V}\right)\right)\to ⟨{x},{y}⟩\in \left({A}×{A}\right)$
16 3 15 relssi ${⊢}\mathrm{I}\cap \left({A}×\mathrm{V}\right)\subseteq {A}×{A}$
17 2 16 ssini ${⊢}\mathrm{I}\cap \left({A}×\mathrm{V}\right)\subseteq \mathrm{I}\cap \left({A}×{A}\right)$
18 ssv ${⊢}{A}\subseteq \mathrm{V}$
19 xpss2 ${⊢}{A}\subseteq \mathrm{V}\to {A}×{A}\subseteq {A}×\mathrm{V}$
20 sslin ${⊢}{A}×{A}\subseteq {A}×\mathrm{V}\to \mathrm{I}\cap \left({A}×{A}\right)\subseteq \mathrm{I}\cap \left({A}×\mathrm{V}\right)$
21 18 19 20 mp2b ${⊢}\mathrm{I}\cap \left({A}×{A}\right)\subseteq \mathrm{I}\cap \left({A}×\mathrm{V}\right)$
22 17 21 eqssi ${⊢}\mathrm{I}\cap \left({A}×\mathrm{V}\right)=\mathrm{I}\cap \left({A}×{A}\right)$
23 1 22 eqtri ${⊢}{\mathrm{I}↾}_{{A}}=\mathrm{I}\cap \left({A}×{A}\right)$