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 e. _V
	opeqsn.2	|- B e. _V
Assertion	opeqsn	|- ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) )

Proof

Step	Hyp	Ref	Expression
1		opeqsn.1	|- A e. _V
2		opeqsn.2	|- B e. _V
3		opeqsng	|- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) ) )
4	1 2 3	mp2an	|- ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) )