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 ↾ { 𝐴 } ) = ( { 𝐴 } × { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( I ↾ { 𝐴 } )
2		relxp	⊢ Rel ( { 𝐴 } × { 𝐴 } )
3		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
4		velsn	⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
5	3 4	anbi12i	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
6		vex	⊢ 𝑦 ∈ V
7	6	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
8	3 7	anbi12i	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑥 = 𝑦 ) )
9		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝑦 ) )
10		eqcom	⊢ ( 𝐴 = 𝑦 ↔ 𝑦 = 𝐴 )
11	9 10	bitrdi	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑦 = 𝐴 ) )
12	11	pm5.32i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
13	8 12	bitri	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
14		df-br	⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
15	14	anbi2i	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
16	5 13 15	3bitr2ri	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) )
17	6	opelresi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ { 𝐴 } ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
18		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝐴 } × { 𝐴 } ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) )
19	16 17 18	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ { 𝐴 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝐴 } × { 𝐴 } ) )
20	1 2 19	eqrelriiv	⊢ ( I ↾ { 𝐴 } ) = ( { 𝐴 } × { 𝐴 } )