Metamath Proof Explorer

Theorem un0

Description: The union of a class with the empty set is itself. Theorem 24 of Suppes p. 27. (Contributed by NM, 15-Jul-1993)

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

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. x e. (/)
2 1 biorfi 
 |-  ( x e. A <-> ( x e. A \/ x e. (/) ) )
3 2 bicomi 
 |-  ( ( x e. A \/ x e. (/) ) <-> x e. A )
4 3 uneqri 
 |-  ( A u. (/) ) = A