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 } )