Theorem preqsn

Description: Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008) (Revised by AV, 12-Jun-2022)

	Ref	Expression
Hypotheses	preqsn.1	|- A e. _V
	preqsn.2	|- B e. _V
Assertion	preqsn	|- ( { A , B } = { C } <-> ( A = B /\ B = C ) )

Proof

Step	Hyp	Ref	Expression
1		preqsn.1	|- A e. _V
2		preqsn.2	|- B e. _V
3		id	|- ( A e. _V -> A e. _V )
4	2	a1i	|- ( A e. _V -> B e. _V )
5	3 4	preqsnd	|- ( A e. _V -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
6	1 5	ax-mp	|- ( { A , B } = { C } <-> ( A = C /\ B = C ) )
7		eqeq2	|- ( B = C -> ( A = B <-> A = C ) )
8	7	pm5.32ri	|- ( ( A = B /\ B = C ) <-> ( A = C /\ B = C ) )
9	6 8	bitr4i	|- ( { A , B } = { C } <-> ( A = B /\ B = C ) )