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

Proof

Step Hyp Ref Expression
1 mapvalg A V B W A B = g | g : B A
2 1 eleq2d A V B W C A B C g | g : B A
3 fex2 C : B A B W A V C V
4 3 3com13 A V B W C : B A C V
5 4 3expia A V B W C : B A C V
6 feq1 g = C g : B A C : B A
7 6 elab3g C : B A C V C g | g : B A C : B A
8 5 7 syl A V B W C g | g : B A C : B A
9 2 8 bitrd A V B W C A B C : B A