Metamath Proof Explorer


Theorem elmapg

Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion elmapg AVBWCABC:BA

Proof

Step Hyp Ref Expression
1 mapvalg AVBWAB=g|g:BA
2 1 eleq2d AVBWCABCg|g:BA
3 fex2 C:BABWAVCV
4 3 3com13 AVBWC:BACV
5 4 3expia AVBWC:BACV
6 feq1 g=Cg:BAC:BA
7 6 elab3g C:BACVCg|g:BAC:BA
8 5 7 syl AVBWCg|g:BAC:BA
9 2 8 bitrd AVBWCABC:BA