Theorem preq1i

Description: Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012)

	Ref	Expression
Hypothesis	preq1i.1	|- A = B
Assertion	preq1i	|- { A , C } = { B , C }

Proof

Step	Hyp	Ref	Expression
1		preq1i.1	|- A = B
2		preq1	|- ( A = B -> { A , C } = { B , C } )
3	1 2	ax-mp	|- { A , C } = { B , C }