Metamath Proof Explorer

Theorem eqcomi

Description: Inference from commutative law for class equality. (Contributed by NM, 26-May-1993)

Ref Expression
Hypothesis eqcomi.1 
|- A = B
Assertion eqcomi 
|- B = A

Proof

Step Hyp Ref Expression
1 eqcomi.1 
 |-  A = B
2 eqcom 
 |-  ( A = B <-> B = A )
3 1 2 mpbi 
 |-  B = A