Metamath Proof Explorer


Theorem preq1

Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998)

Ref Expression
Assertion preq1 A = B A C = B C

Proof

Step Hyp Ref Expression
1 sneq A = B A = B
2 1 uneq1d A = B A C = B C
3 df-pr A C = A C
4 df-pr B C = B C
5 2 3 4 3eqtr4g A = B A C = B C