Metamath Proof Explorer


Theorem mapss

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 BVABACBC

Proof

Step Hyp Ref Expression
1 elmapi fACf:CA
2 1 adantl BVABfACf:CA
3 simplr BVABfACAB
4 2 3 fssd BVABfACf:CB
5 simpll BVABfACBV
6 elmapex fACAVCV
7 6 simprd fACCV
8 7 adantl BVABfACCV
9 5 8 elmapd BVABfACfBCf:CB
10 4 9 mpbird BVABfACfBC
11 10 ex BVABfACfBC
12 11 ssrdv BVABACBC