Description: Inference from commutative law for class equality. (Contributed by NM, 26May1993)
Ref  Expression  

Hypothesis  eqcomi.1   A = B 

Assertion  eqcomi   B = A 
Step  Hyp  Ref  Expression 

1  eqcomi.1   A = B 

2  eqcom   ( A = B <> B = A ) 

3  1 2  mpbi   B = A 