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\} \times \{A\}$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({I ↾}_{\{A\}})$
2		relxp	$⊢ Rel (\{A\} \times \{A\})$
3		velsn	$⊢ x \in \{A\} \leftrightarrow x = A$
4		velsn	$⊢ y \in \{A\} \leftrightarrow y = A$
5	3 4	anbi12i	$⊢ (x \in \{A\} \land y \in \{A\}) \leftrightarrow (x = A \land y = A)$
6		vex	$⊢ y \in V$
7	6	ideq	$⊢ x I y \leftrightarrow x = y$
8	3 7	anbi12i	$⊢ (x \in \{A\} \land x I y) \leftrightarrow (x = A \land x = y)$
9		eqeq1	$⊢ x = A \to (x = y \leftrightarrow A = y)$
10		eqcom	$⊢ A = y \leftrightarrow y = A$
11	9 10	bitrdi	$⊢ x = A \to (x = y \leftrightarrow y = A)$
12	11	pm5.32i	$⊢ (x = A \land x = y) \leftrightarrow (x = A \land y = A)$
13	8 12	bitri	$⊢ (x \in \{A\} \land x I y) \leftrightarrow (x = A \land y = A)$
14		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
15	14	anbi2i	$⊢ (x \in \{A\} \land x I y) \leftrightarrow (x \in \{A\} \land ⟨x, y⟩ \in I)$
16	5 13 15	3bitr2ri	$⊢ (x \in \{A\} \land ⟨x, y⟩ \in I) \leftrightarrow (x \in \{A\} \land y \in \{A\})$
17	6	opelresi	$⊢ ⟨x, y⟩ \in ({I ↾}_{\{A\}}) \leftrightarrow (x \in \{A\} \land ⟨x, y⟩ \in I)$
18		opelxp	$⊢ ⟨x, y⟩ \in (\{A\} \times \{A\}) \leftrightarrow (x \in \{A\} \land y \in \{A\})$
19	16 17 18	3bitr4i	$⊢ ⟨x, y⟩ \in ({I ↾}_{\{A\}}) \leftrightarrow ⟨x, y⟩ \in (\{A\} \times \{A\})$
20	1 2 19	eqrelriiv	$⊢ {I ↾}_{\{A\}} = \{A\} \times \{A\}$

Metamath Proof Explorer

Theorem restidsing

Proof