Description: Subset theorem for the well-founded predicate. Exercise 1 of TakeutiZaring p. 31. (Contributed by NM, 3-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | frss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 | |
|
2 | 1 | com12 | |
3 | 2 | anim1d | |
4 | 3 | imim1d | |
5 | 4 | alimdv | |
6 | df-fr | |
|
7 | df-fr | |
|
8 | 5 6 7 | 3imtr4g | |