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 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
df-v |
|
2 |
|
equid |
|
3 |
|
elirrv |
|
4 |
3
|
nelir |
|
5 |
2 4
|
2th |
|
6 |
5
|
abbii |
|
7 |
1 6
|
eqtr2i |
|