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