Theorem dfid2

Description: Alternate definition of the identity relation. Instance of dfid3 not requiring auxiliary axioms. (Contributed by NM, 15-Mar-2007) Reduce axiom usage. (Revised by Gino Giotto, 4-Nov-2024) (Proof shortened by BJ, 5-Nov-2024)

Use df-id instead to make the semantics of the constructor df-opab clearer. (New usage is discouraged.)

	Ref	Expression
Assertion	dfid2	|- _I = { <. x , x >. | x = x }

Proof

Step	Hyp	Ref	Expression
1		df-id	|- _I = { <. x , y >. | x = y }
2		equcomi	|- ( x = y -> y = x )
3	2	opeq2d	|- ( x = y -> <. x , y >. = <. x , x >. )
4	3	eqeq2d	|- ( x = y -> ( z = <. x , y >. <-> z = <. x , x >. ) )
5	4	pm5.32ri	|- ( ( z = <. x , y >. /\ x = y ) <-> ( z = <. x , x >. /\ x = y ) )
6	5	exbii	|- ( E. y ( z = <. x , y >. /\ x = y ) <-> E. y ( z = <. x , x >. /\ x = y ) )
7		ax6evr	|- E. y x = y
8		19.42v	|- ( E. y ( z = <. x , x >. /\ x = y ) <-> ( z = <. x , x >. /\ E. y x = y ) )
9	7 8	mpbiran2	|- ( E. y ( z = <. x , x >. /\ x = y ) <-> z = <. x , x >. )
10	6 9	bitri	|- ( E. y ( z = <. x , y >. /\ x = y ) <-> z = <. x , x >. )
11		eqidd	|- ( z = <. x , x >. -> x = x )
12	11	pm4.71i	|- ( z = <. x , x >. <-> ( z = <. x , x >. /\ x = x ) )
13	10 12	bitri	|- ( E. y ( z = <. x , y >. /\ x = y ) <-> ( z = <. x , x >. /\ x = x ) )
14	13	exbii	|- ( E. x E. y ( z = <. x , y >. /\ x = y ) <-> E. x ( z = <. x , x >. /\ x = x ) )
15		id	|- ( x = u -> x = u )
16	15 15	opeq12d	|- ( x = u -> <. x , x >. = <. u , u >. )
17	16	eqeq2d	|- ( x = u -> ( z = <. x , x >. <-> z = <. u , u >. ) )
18	15 15	eqeq12d	|- ( x = u -> ( x = x <-> u = u ) )
19	17 18	anbi12d	|- ( x = u -> ( ( z = <. x , x >. /\ x = x ) <-> ( z = <. u , u >. /\ u = u ) ) )
20	19	exexw	|- ( E. x ( z = <. x , x >. /\ x = x ) <-> E. x E. x ( z = <. x , x >. /\ x = x ) )
21	14 20	bitri	|- ( E. x E. y ( z = <. x , y >. /\ x = y ) <-> E. x E. x ( z = <. x , x >. /\ x = x ) )
22	21	abbii	|- { z | E. x E. y ( z = <. x , y >. /\ x = y ) } = { z | E. x E. x ( z = <. x , x >. /\ x = x ) }
23		df-opab	|- { <. x , y >. | x = y } = { z | E. x E. y ( z = <. x , y >. /\ x = y ) }
24		df-opab	|- { <. x , x >. | x = x } = { z | E. x E. x ( z = <. x , x >. /\ x = x ) }
25	22 23 24	3eqtr4i	|- { <. x , y >. | x = y } = { <. x , x >. | x = x }
26	1 25	eqtri	|- _I = { <. x , x >. | x = x }