Metamath Proof Explorer

Theorem bj-dfid2ALT

Description: Alternate version of dfid2 . (Contributed by BJ, 9-Nov-2024) (Proof modification is discouraged.) Use df-id instead to make the semantics of the construction df-opab clearer. (New usage is discouraged.)

Ref Expression
Assertion bj-dfid2ALT 
|- _I = { <. x , x >. | T. }

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 10 exbii 
 |-  ( E. x E. y ( z = <. x , y >. /\ x = y ) <-> E. x z = <. x , x >. )
12 id 
 |-  ( x = u -> x = u )
13 12 12 opeq12d 
 |-  ( x = u -> <. x , x >. = <. u , u >. )
14 13 eqeq2d 
 |-  ( x = u -> ( z = <. x , x >. <-> z = <. u , u >. ) )
15 14 exexw 
 |-  ( E. x z = <. x , x >. <-> E. x E. x z = <. x , x >. )
16 11 15 bitri 
 |-  ( E. x E. y ( z = <. x , y >. /\ x = y ) <-> E. x E. x z = <. x , x >. )
17 tru 
 |-  T.
18 17 biantru 
 |-  ( z = <. x , x >. <-> ( z = <. x , x >. /\ T. ) )
19 18 exbii 
 |-  ( E. x z = <. x , x >. <-> E. x ( z = <. x , x >. /\ T. ) )
20 19 exbii 
 |-  ( E. x E. x z = <. x , x >. <-> E. x E. x ( z = <. x , x >. /\ T. ) )
21 16 20 bitri 
 |-  ( E. x E. y ( z = <. x , y >. /\ x = y ) <-> E. x E. x ( z = <. x , x >. /\ T. ) )
22 21 abbii 
 |-  { z | E. x E. y ( z = <. x , y >. /\ x = y ) } = { z | E. x E. x ( z = <. x , x >. /\ T. ) }
23 df-opab 
 |-  { <. x , y >. | x = y } = { z | E. x E. y ( z = <. x , y >. /\ x = y ) }
24 df-opab 
 |-  { <. x , x >. | T. } = { z | E. x E. x ( z = <. x , x >. /\ T. ) }
25 22 23 24 3eqtr4i 
 |-  { <. x , y >. | x = y } = { <. x , x >. | T. }
26 1 25 eqtri 
 |-  _I = { <. x , x >. | T. }