Metamath Proof Explorer

Theorem uneq2

Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993)

Ref Expression
Assertion uneq2 
|- ( A = B -> ( C u. A ) = ( C u. B ) )

Proof

Step Hyp Ref Expression
1 uneq1 
 |-  ( A = B -> ( A u. C ) = ( B u. C ) )
2 uncom 
 |-  ( C u. A ) = ( A u. C )
3 uncom 
 |-  ( C u. B ) = ( B u. C )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> ( C u. A ) = ( C u. B ) )