Metamath Proof Explorer

Theorem unidm

Description: Idempotent law for union of classes. Theorem 23 of Suppes p. 27. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion unidm 
|- ( A u. A ) = A

Proof

Step Hyp Ref Expression
1 oridm 
 |-  ( ( x e. A \/ x e. A ) <-> x e. A )
2 1 uneqri 
 |-  ( A u. A ) = A