Metamath Proof Explorer

Theorem ruv

Description: The Russell class is equal to the universe _V . Exercise 5 of TakeutiZaring p. 22. (Contributed by Alan Sare, 4-Oct-2008)

Ref Expression
Assertion ruv 
|- { x | x e/ x } = _V

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 elirr 
 |-  -. x e. x
3 2 nelir 
 |-  x e/ x
4 1 3 2th 
 |-  ( x e. _V <-> x e/ x )
5 4 eqabi 
 |-  _V = { x | x e/ x }
6 5 eqcomi 
 |-  { x | x e/ x } = _V