Metamath Proof Explorer


Theorem snopeqopsnid

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

Proof

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