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