Metamath Proof Explorer


Theorem preq12

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

Ref Expression
Assertion preq12 A = C B = D A B = C D

Proof

Step Hyp Ref Expression
1 preq1 A = C A B = C B
2 preq2 B = D C B = C D
3 1 2 sylan9eq A = C B = D A B = C D