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

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ I ↾ A
2 relxp ⊢ Rel ⁡ A × A
3 velsn ⊢ x ∈ A ↔ x = A
4 velsn ⊢ y ∈ A ↔ y = A
5 3 4 anbi12i ⊢ x ∈ A ∧ y ∈ A ↔ x = A ∧ y = A
6 vex ⊢ y ∈ V
7 6 ideq ⊢ x I y ↔ x = y
8 3 7 anbi12i ⊢ x ∈ 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 ∈ A ∧ x I y ↔ x = A ∧ y = A
14 df-br ⊢ x I y ↔ x y ∈ I
15 14 anbi2i ⊢ x ∈ A ∧ x I y ↔ x ∈ A ∧ x y ∈ I
16 5 13 15 3bitr2ri ⊢ x ∈ A ∧ x y ∈ I ↔ x ∈ A ∧ y ∈ A
17 6 opelresi ⊢ x y ∈ I ↾ A ↔ x ∈ A ∧ x y ∈ I
18 opelxp ⊢ x y ∈ A × A ↔ x ∈ A ∧ y ∈ A
19 16 17 18 3bitr4i ⊢ x y ∈ I ↾ A ↔ x y ∈ A × A
20 1 2 19 eqrelriiv ⊢ I ↾ A = A × A