Metamath Proof Explorer

Theorem preq2

Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion preq2 
|- ( A = B -> { C , A } = { C , B } )

Proof

Step Hyp Ref Expression
1 preq1 
 |-  ( A = B -> { A , C } = { B , C } )
2 prcom 
 |-  { C , A } = { A , C }
3 prcom 
 |-  { C , B } = { B , C }
4 1 2 3 3eqtr4g 
 |-  ( A = B -> { C , A } = { C , B } )