Metamath Proof Explorer

Theorem ffdm

Description: A mapping is a partial function. (Contributed by NM, 25-Nov-2007)

Ref Expression
Assertion ffdm ⊢ F : A ⟶ B → F : dom ⁡ F ⟶ B ∧ dom ⁡ F ⊆ A

Proof

Step Hyp Ref Expression
1 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
2 1 feq2d ⊢ F : A ⟶ B → F : dom ⁡ F ⟶ B ↔ F : A ⟶ B
3 2 ibir ⊢ F : A ⟶ B → F : dom ⁡ F ⟶ B
4 eqimss ⊢ dom ⁡ F = A → dom ⁡ F ⊆ A
5 1 4 syl ⊢ F : A ⟶ B → dom ⁡ F ⊆ A
6 3 5 jca ⊢ F : A ⟶ B → F : dom ⁡ F ⟶ B ∧ dom ⁡ F ⊆ A