This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )

Proof

Step Hyp Ref Expression
1 funimass4 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ) )
2 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
3 2 elsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 )
4 3 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 )
5 1 4 bitr2di ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ ( 𝐹 “ 𝐴 ) ⊆ { 𝐵 } ) )
6 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ { 𝐵 } ↔ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )
7 5 6 bitrd ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )