Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013) (Revised by Thierry Arnoux, 10-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mptfnd.1 | ⊢ Ⅎ 𝑥 𝐴 | |
mptfnd.2 | ⊢ Ⅎ 𝑥 𝜑 | ||
mptfnd.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) | ||
Assertion | mptfnd | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mptfnd.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | mptfnd.2 | ⊢ Ⅎ 𝑥 𝜑 | |
3 | mptfnd.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) | |
4 | 3 | ex | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉 ) ) |
5 | elex | ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V ) | |
6 | 4 5 | syl6 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ V ) ) |
7 | 2 6 | ralrimi | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
8 | 1 | mptfnf | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) |
9 | 7 8 | sylib | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) |