Description: Equality deduction for unordered pairs. (Contributed by NM, 19Oct2012)
Ref  Expression  

Hypothesis  preq1d.1   ( ph > A = B ) 

Assertion  preq2d   ( ph > { C , A } = { C , B } ) 
Step  Hyp  Ref  Expression 

1  preq1d.1   ( ph > A = B ) 

2  preq2   ( A = B > { C , A } = { C , B } ) 

3  1 2  syl   ( ph > { C , A } = { C , B } ) 