Theorem restidsing

Description: Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009) (Proof shortened by JJ, 25-Aug-2021) (Proof shortened by Peter Mazsa, 6-Oct-2022)

	Ref	Expression
Assertion	restidsing	|- ( _I |` { A } ) = ( { A } X. { A } )

Proof

Step	Hyp	Ref	Expression
1		relres	|- Rel ( _I |` { A } )
2		relxp	|- Rel ( { A } X. { A } )
3		velsn	|- ( x e. { A } <-> x = A )
4		velsn	|- ( y e. { A } <-> y = A )
5	3 4	anbi12i	|- ( ( x e. { A } /\ y e. { A } ) <-> ( x = A /\ y = A ) )
6		vex	|- y e. _V
7	6	ideq	|- ( x _I y <-> x = y )
8	3 7	anbi12i	|- ( ( x e. { A } /\ x _I y ) <-> ( x = A /\ x = y ) )
9		eqeq1	|- ( x = A -> ( x = y <-> A = y ) )
10		eqcom	|- ( A = y <-> y = A )
11	9 10	bitrdi	|- ( x = A -> ( x = y <-> y = A ) )
12	11	pm5.32i	|- ( ( x = A /\ x = y ) <-> ( x = A /\ y = A ) )
13	8 12	bitri	|- ( ( x e. { A } /\ x _I y ) <-> ( x = A /\ y = A ) )
14		df-br	|- ( x _I y <-> <. x , y >. e. _I )
15	14	anbi2i	|- ( ( x e. { A } /\ x _I y ) <-> ( x e. { A } /\ <. x , y >. e. _I ) )
16	5 13 15	3bitr2ri	|- ( ( x e. { A } /\ <. x , y >. e. _I ) <-> ( x e. { A } /\ y e. { A } ) )
17	6	opelresi	|- ( <. x , y >. e. ( _I |` { A } ) <-> ( x e. { A } /\ <. x , y >. e. _I ) )
18		opelxp	|- ( <. x , y >. e. ( { A } X. { A } ) <-> ( x e. { A } /\ y e. { A } ) )
19	16 17 18	3bitr4i	|- ( <. x , y >. e. ( _I |` { A } ) <-> <. x , y >. e. ( { A } X. { A } ) )
20	1 2 19	eqrelriiv	|- ( _I |` { A } ) = ( { A } X. { A } )