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

Metamath Proof Explorer

Theorem opabresid

Description: The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012)

		Ref	Expression
	Assertion	opabresid	$⊢ {I ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y = x)\}$

Step	Hyp	Ref	Expression
1		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
2		equcom	$⊢ x = y \leftrightarrow y = x$
3	2	opabbii	$⊢ \{⟨x, y⟩ \| x = y\} = \{⟨x, y⟩ \| y = x\}$
4	1 3	eqtri	$⊢ I = \{⟨x, y⟩ \| y = x\}$
5	4	reseq1i	$⊢ {I ↾}_{A} = {\{⟨x, y⟩ \| y = x\} ↾}_{A}$
6		resopab	$⊢ {\{⟨x, y⟩ \| y = x\} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y = x)\}$
7	5 6	eqtri	$⊢ {I ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y = x)\}$