Metamath Proof Explorer

Theorem univ

Description: The union of the universe is the universe. Exercise 4.12(c) of Mendelson p. 235. (Contributed by NM, 14-Sep-2003)

Ref Expression
Assertion univ 
|- U. _V = _V

Proof

Step Hyp Ref Expression
1 pwv 
 |-  ~P _V = _V
2 1 unieqi 
 |-  U. ~P _V = U. _V
3 unipw 
 |-  U. ~P _V = _V
4 2 3 eqtr3i 
 |-  U. _V = _V