Theorem dfid7

Description: Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020)

	Ref	Expression
Assertion	dfid7	|- _I = ( x e. _V |-> |^| { y | ( x C_ y /\ T. ) } )

Proof

Step	Hyp	Ref	Expression
1		dfid4	|- _I = ( x e. _V |-> x )
2		ancom	|- ( ( x C_ y /\ T. ) <-> ( T. /\ x C_ y ) )
3		truan	|- ( ( T. /\ x C_ y ) <-> x C_ y )
4	2 3	bitri	|- ( ( x C_ y /\ T. ) <-> x C_ y )
5	4	abbii	|- { y | ( x C_ y /\ T. ) } = { y | x C_ y }
6	5	inteqi	|- |^| { y | ( x C_ y /\ T. ) } = |^| { y | x C_ y }
7		vex	|- x e. _V
8	7	intmin2	|- |^| { y | x C_ y } = x
9	6 8	eqtri	|- |^| { y | ( x C_ y /\ T. ) } = x
10	9	mpteq2i	|- ( x e. _V |-> |^| { y | ( x C_ y /\ T. ) } ) = ( x e. _V |-> x )
11	1 10	eqtr4i	|- _I = ( x e. _V |-> |^| { y | ( x C_ y /\ T. ) } )