Description: The union of a class with the universal class is the universal class. Exercise 4.10(l) of Mendelson p. 231. (Contributed by NM, 17-May-1998)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unv | |- ( A u. _V ) = _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssv | |- ( A u. _V ) C_ _V |
|
| 2 | ssun2 | |- _V C_ ( A u. _V ) |
|
| 3 | 1 2 | eqssi | |- ( A u. _V ) = _V |