Theorem preqr1

Description: Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995)

	Ref	Expression
Hypotheses	preqr1.a	|- A e. _V
	preqr1.b	|- B e. _V
Assertion	preqr1	|- ( { A , C } = { B , C } -> A = B )

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	|- A e. _V
2		preqr1.b	|- B e. _V
3		id	|- ( A e. _V -> A e. _V )
4	2	a1i	|- ( A e. _V -> B e. _V )
5	3 4	preq1b	|- ( A e. _V -> ( { A , C } = { B , C } <-> A = B ) )
6	1 5	ax-mp	|- ( { A , C } = { B , C } <-> A = B )
7	6	biimpi	|- ( { A , C } = { B , C } -> A = B )