Metamath Proof Explorer

Theorem 0un

Description: The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion 0un 
|- ( (/) u. A ) = A

Proof

Step Hyp Ref Expression
1 uncom 
 |-  ( (/) u. A ) = ( A u. (/) )
2 un0 
 |-  ( A u. (/) ) = A
3 1 2 eqtri 
 |-  ( (/) u. A ) = A