Theorem opeqsn

Description: Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	opeqsn.1	$$⊢A\in \mathrm{V}$$
	opeqsn.2	$$⊢B\in \mathrm{V}$$
Assertion	opeqsn	$$⊢⟨A,B⟩=\left\{C\right\}\leftrightarrow \left(A=B\wedge C=\left\{A\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		opeqsn.1	$$⊢A\in \mathrm{V}$$
2		opeqsn.2	$$⊢B\in \mathrm{V}$$
3		opeqsng	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(⟨A,B⟩=\left\{C\right\}\leftrightarrow \left(A=B\wedge C=\left\{A\right\}\right)\right)$$
4	1 2 3	mp2an	$$⊢⟨A,B⟩=\left\{C\right\}\leftrightarrow \left(A=B\wedge C=\left\{A\right\}\right)$$