Description: Subset inheritance for set exponentiation. Theorem 99 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 26-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | mapss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmapi | |
|
2 | 1 | adantl | |
3 | simplr | |
|
4 | 2 3 | fssd | |
5 | simpll | |
|
6 | elmapex | |
|
7 | 6 | simprd | |
8 | 7 | adantl | |
9 | 5 8 | elmapd | |
10 | 4 9 | mpbird | |
11 | 10 | ex | |
12 | 11 | ssrdv | |