Metamath Proof Explorer


Theorem opidg

Description: The ordered pair <. A , A >. in Kuratowski's representation. Closed form of opid . (Contributed by Peter Mazsa, 22-Jul-2019) (Avoid depending on this detail.)

Ref Expression
Assertion opidg
|- ( A e. V -> <. A , A >. = { { A } } )

Proof

Step Hyp Ref Expression
1 dfopg
 |-  ( ( A e. V /\ A e. V ) -> <. A , A >. = { { A } , { A , A } } )
2 1 anidms
 |-  ( A e. V -> <. A , A >. = { { A } , { A , A } } )
3 dfsn2
 |-  { A } = { A , A }
4 3 eqcomi
 |-  { A , A } = { A }
5 4 preq2i
 |-  { { A } , { A , A } } = { { A } , { A } }
6 dfsn2
 |-  { { A } } = { { A } , { A } }
7 5 6 eqtr4i
 |-  { { A } , { A , A } } = { { A } }
8 2 7 eqtrdi
 |-  ( A e. V -> <. A , A >. = { { A } } )