Description: If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006) (Proof shortened by Andrew Salmon, 17-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | dmfex | ⊢ ( ( 𝐹 ∈ 𝐶 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐴 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdm | ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 ) | |
2 | dmexg | ⊢ ( 𝐹 ∈ 𝐶 → dom 𝐹 ∈ V ) | |
3 | eleq1 | ⊢ ( dom 𝐹 = 𝐴 → ( dom 𝐹 ∈ V ↔ 𝐴 ∈ V ) ) | |
4 | 2 3 | syl5ib | ⊢ ( dom 𝐹 = 𝐴 → ( 𝐹 ∈ 𝐶 → 𝐴 ∈ V ) ) |
5 | 1 4 | syl | ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ∈ 𝐶 → 𝐴 ∈ V ) ) |
6 | 5 | impcom | ⊢ ( ( 𝐹 ∈ 𝐶 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐴 ∈ V ) |