Theorem dfid4

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

	Ref	Expression
Assertion	dfid4	|- _I = ( x e. _V |-> x )

Proof

Step	Hyp	Ref	Expression
1		equcom	|- ( x = y <-> y = x )
2		vex	|- x e. _V
3	2	biantrur	|- ( y = x <-> ( x e. _V /\ y = x ) )
4	1 3	bitri	|- ( x = y <-> ( x e. _V /\ y = x ) )
5	4	opabbii	|- { <. x , y >. | x = y } = { <. x , y >. | ( x e. _V /\ y = x ) }
6		df-id	|- _I = { <. x , y >. | x = y }
7		df-mpt	|- ( x e. _V |-> x ) = { <. x , y >. | ( x e. _V /\ y = x ) }
8	5 6 7	3eqtr4i	|- _I = ( x e. _V |-> x )