This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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