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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mapvalg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ↑m 𝐵 ) = { 𝑔 ∣ 𝑔 : 𝐵 ⟶ 𝐴 } )
2	1	eleq2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐶 ∈ { 𝑔 ∣ 𝑔 : 𝐵 ⟶ 𝐴 } ) )
3		fex2	⊢ ( ( 𝐶 : 𝐵 ⟶ 𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → 𝐶 ∈ V )
4	3	3com13	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 : 𝐵 ⟶ 𝐴 ) → 𝐶 ∈ V )
5	4	3expia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐶 : 𝐵 ⟶ 𝐴 → 𝐶 ∈ V ) )
6		feq1	⊢ ( 𝑔 = 𝐶 → ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )
7	6	elab3g	⊢ ( ( 𝐶 : 𝐵 ⟶ 𝐴 → 𝐶 ∈ V ) → ( 𝐶 ∈ { 𝑔 ∣ 𝑔 : 𝐵 ⟶ 𝐴 } ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )
8	5 7	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐶 ∈ { 𝑔 ∣ 𝑔 : 𝐵 ⟶ 𝐴 } ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )
9	2 8	bitrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐶 : 𝐵 ⟶ 𝐴 ) )