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\in \mathrm{V}$$
Assertion	snopeqopsnid	$$⊢\left\{⟨A,A⟩\right\}=⟨\left\{A\right\},\left\{A\right\}⟩$$

Proof

Step	Hyp	Ref	Expression
1		snopeqopsnid.a	$$⊢A\in \mathrm{V}$$
2		eqid	$$⊢A=A$$
3		eqid	$$⊢\left\{A\right\}=\left\{A\right\}$$
4	1 1	snopeqop	$$⊢\left\{⟨A,A⟩\right\}=⟨\left\{A\right\},\left\{A\right\}⟩\leftrightarrow \left(A=A\wedge \left\{A\right\}=\left\{A\right\}\wedge \left\{A\right\}=\left\{A\right\}\right)$$
5	2 3 3 4	mpbir3an	$$⊢\left\{⟨A,A⟩\right\}=⟨\left\{A\right\},\left\{A\right\}⟩$$