This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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