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 }