Description: The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | r1sssuc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r1tr | ||
2 | dftr4 | ||
3 | 1 2 | mpbi | |
4 | r1suc | ||
5 | 3 4 | sseqtrrid |