Metamath Proof Explorer

Theorem funconstss

Description: Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007)

Ref Expression
Assertion funconstss ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → ∀ x ∈ A F ⁡ x = B ↔ A ⊆ F -1 B

Proof

Step Hyp Ref Expression
1 funimass4 ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ ∀ x ∈ A F ⁡ x ∈ B
2 fvex ⊢ F ⁡ x ∈ V
3 2 elsn ⊢ F ⁡ x ∈ B ↔ F ⁡ x = B
4 3 ralbii ⊢ ∀ x ∈ A F ⁡ x ∈ B ↔ ∀ x ∈ A F ⁡ x = B
5 1 4 bitr2di ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → ∀ x ∈ A F ⁡ x = B ↔ F A ⊆ B
6 funimass3 ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ A ⊆ F -1 B
7 5 6 bitrd ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → ∀ x ∈ A F ⁡ x = B ↔ A ⊆ F -1 B