This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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