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

Metamath Proof Explorer

Theorem dfid4

Description: The identity function expressed using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017)

		Ref	Expression
	Assertion	dfid4	$⊢ I = (x \in V ⟼ x)$

Step	Hyp	Ref	Expression
1		equcom	$⊢ x = y \leftrightarrow y = x$
2		vex	$⊢ x \in V$
3	2	biantrur	$⊢ y = x \leftrightarrow (x \in V \land y = x)$
4	1 3	bitri	$⊢ x = y \leftrightarrow (x \in V \land y = x)$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| x = y\} = \{⟨x, y⟩ \| (x \in V \land y = x)\}$
6		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
7		df-mpt	$⊢ (x \in V ⟼ x) = \{⟨x, y⟩ \| (x \in V \land y = x)\}$
8	5 6 7	3eqtr4i	$⊢ I = (x \in V ⟼ x)$