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 } } ) |
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 } } ) |