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