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 V
Assertion snopeqopsnid A A = A A

Proof

Step Hyp Ref Expression
1 snopeqopsnid.a A 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