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 } u. { C } ) = ( { B } u. { C } ) )
3 df-pr 
 |-  { A , C } = ( { A } u. { C } )
4 df-pr 
 |-  { B , C } = ( { B } u. { C } )
5 2 3 4 3eqtr4g 
 |-  ( A = B -> { A , C } = { B , C } )