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

Metamath Proof Explorer

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 } )