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	⊢ 𝐴 ∈ V
Assertion	snopeqopsnid	⊢ { ⟨ 𝐴 , 𝐴 ⟩ } = ⟨ { 𝐴 } , { 𝐴 } ⟩

Proof

Step	Hyp	Ref	Expression
1		snopeqopsnid.a	⊢ 𝐴 ∈ V
2		eqid	⊢ 𝐴 = 𝐴
3		eqid	⊢ { 𝐴 } = { 𝐴 }
4	1 1	snopeqop	⊢ ( { ⟨ 𝐴 , 𝐴 ⟩ } = ⟨ { 𝐴 } , { 𝐴 } ⟩ ↔ ( 𝐴 = 𝐴 ∧ { 𝐴 } = { 𝐴 } ∧ { 𝐴 } = { 𝐴 } ) )
5	2 3 3 4	mpbir3an	⊢ { ⟨ 𝐴 , 𝐴 ⟩ } = ⟨ { 𝐴 } , { 𝐴 } ⟩