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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-v | |- _V = { x | x = x } |
|
2 | equid | |- x = x |
|
3 | elirrv | |- -. x e. x |
|
4 | 3 | nelir | |- x e/ x |
5 | 2 4 | 2th | |- ( x = x <-> x e/ x ) |
6 | 5 | abbii | |- { x | x = x } = { x | x e/ x } |
7 | 1 6 | eqtr2i | |- { x | x e/ x } = _V |