Metamath Proof Explorer


Theorem preq12i

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

Ref Expression
Hypotheses preq1i.1
|- A = B
preq12i.2
|- C = D
Assertion preq12i
|- { A , C } = { B , D }

Proof

Step Hyp Ref Expression
1 preq1i.1
 |-  A = B
2 preq12i.2
 |-  C = D
3 preq12
 |-  ( ( A = B /\ C = D ) -> { A , C } = { B , D } )
4 1 2 3 mp2an
 |-  { A , C } = { B , D }