Metamath Proof Explorer


Theorem unv

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 V = V

Proof

Step Hyp Ref Expression
1 ssv A V V
2 ssun2 V A V
3 1 2 eqssi A V = V