Description: Equivalence for an ordered pair of two identical singletons equal to a singleton of an ordered pair. (Contributed by AV, 24-Sep-2020) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | snopeqopsnid.a | |- A e. _V |
|
| Assertion | snopeqopsnid | |- { <. A , A >. } = <. { A } , { A } >. |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snopeqopsnid.a | |- A e. _V |
|
| 2 | eqid | |- A = A |
|
| 3 | eqid | |- { A } = { A } |
|
| 4 | 1 1 | snopeqop | |- ( { <. A , A >. } = <. { A } , { A } >. <-> ( A = A /\ { A } = { A } /\ { A } = { A } ) ) |
| 5 | 2 3 3 4 | mpbir3an | |- { <. A , A >. } = <. { A } , { A } >. |