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 IA=IA×A

Proof

Step Hyp Ref Expression
1 df-res IA=IA×V
2 inss1 IA×VI
3 relinxp RelIA×V
4 elin xyIA×VxyIxyA×V
5 bj-opelidb1 xyIxVx=y
6 5 simprbi xyIx=y
7 opelxp1 xyA×VxA
8 simpr x=yxAxA
9 eleq1w x=yxAyA
10 9 biimpa x=yxAyA
11 8 10 jca x=yxAxAyA
12 6 7 11 syl2an xyIxyA×VxAyA
13 4 12 sylbi xyIA×VxAyA
14 opelxpi xAyAxyA×A
15 13 14 syl xyIA×VxyA×A
16 3 15 relssi IA×VA×A
17 2 16 ssini IA×VIA×A
18 ssv AV
19 xpss2 AVA×AA×V
20 sslin A×AA×VIA×AIA×V
21 18 19 20 mp2b IA×AIA×V
22 17 21 eqssi IA×V=IA×A
23 1 22 eqtri IA=IA×A