Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | elmapi | ⊢ ( 𝐴 ∈ ( 𝐵 ↑_{m} 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmapex | ⊢ ( 𝐴 ∈ ( 𝐵 ↑_{m} 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) | |
2 | elmapg | ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ∈ ( 𝐵 ↑_{m} 𝐶 ) ↔ 𝐴 : 𝐶 ⟶ 𝐵 ) ) | |
3 | 1 2 | syl | ⊢ ( 𝐴 ∈ ( 𝐵 ↑_{m} 𝐶 ) → ( 𝐴 ∈ ( 𝐵 ↑_{m} 𝐶 ) ↔ 𝐴 : 𝐶 ⟶ 𝐵 ) ) |
4 | 3 | ibi | ⊢ ( 𝐴 ∈ ( 𝐵 ↑_{m} 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 ) |