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 B V A B A C B C

Proof

Step Hyp Ref Expression
1 elmapi f A C f : C A
2 1 adantl B V A B f A C f : C A
3 simplr B V A B f A C A B
4 2 3 fssd B V A B f A C f : C B
5 simpll B V A B f A C B V
6 elmapex f A C A V C V
7 6 simprd f A C C V
8 7 adantl B V A B f A C C V
9 5 8 elmapd B V A B f A C f B C f : C B
10 4 9 mpbird B V A B f A C f B C
11 10 ex B V A B f A C f B C
12 11 ssrdv B V A B A C B C