Theorem funsneqopb

Description: A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	funsndifnop.a	$$⊢A\in \mathrm{V}$$
	funsndifnop.b	$$⊢B\in \mathrm{V}$$
	funsndifnop.g	$$⊢G=\left\{⟨A,B⟩\right\}$$
Assertion	funsneqopb	$$⊢A=B\leftrightarrow G\in \left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		funsndifnop.a	$$⊢A\in \mathrm{V}$$
2		funsndifnop.b	$$⊢B\in \mathrm{V}$$
3		funsndifnop.g	$$⊢G=\left\{⟨A,B⟩\right\}$$
4		opeq1	$$⊢A=B\to ⟨A,B⟩=⟨B,B⟩$$
5	4	sneqd	$$⊢A=B\to \left\{⟨A,B⟩\right\}=\left\{⟨B,B⟩\right\}$$
6	2	snopeqopsnid	$$⊢\left\{⟨B,B⟩\right\}=⟨\left\{B\right\},\left\{B\right\}⟩$$
7	5 6	eqtrdi	$$⊢A=B\to \left\{⟨A,B⟩\right\}=⟨\left\{B\right\},\left\{B\right\}⟩$$
8	3 7	syl5eq	$$⊢A=B\to G=⟨\left\{B\right\},\left\{B\right\}⟩$$
9		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
10	9 9	opelvv	$$⊢⟨\left\{B\right\},\left\{B\right\}⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
11	8 10	eqeltrdi	$$⊢A=B\to G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
12	1 2 3	funsndifnop	$$⊢A\ne B\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
13	12	necon4ai	$$⊢G\in \left(\mathrm{V}\times \mathrm{V}\right)\to A=B$$
14	11 13	impbii	$$⊢A=B\leftrightarrow G\in \left(\mathrm{V}\times \mathrm{V}\right)$$