Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011) (Revised by Mario Carneiro, 31-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mptexg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funmpt | ⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
| 2 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
| 3 | 2 | dmmptss | ⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 |
| 4 | ssexg | ⊢ ( ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) | |
| 5 | 3 4 | mpan | ⊢ ( 𝐴 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |
| 6 | funex | ⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) | |
| 7 | 1 5 6 | sylancr | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |