Metamath Proof Explorer


Theorem constmap

Description: A constant (represented without dummy variables) is an element of a function set.

Note: In the following development, we will be quite often quantifying over functions and points in N-dimensional space (which are equivalent to functions from an "index set"). Many of the following theorems exist to transfer standard facts about functions to elements of function sets. (Contributed by Stefan O'Rear, 30-Aug-2014) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Hypotheses constmap.1
|- A e. _V
constmap.3
|- C e. _V
Assertion constmap
|- ( B e. C -> ( A X. { B } ) e. ( C ^m A ) )

Proof

Step Hyp Ref Expression
1 constmap.1
 |-  A e. _V
2 constmap.3
 |-  C e. _V
3 fconst6g
 |-  ( B e. C -> ( A X. { B } ) : A --> C )
4 2 1 elmap
 |-  ( ( A X. { B } ) e. ( C ^m A ) <-> ( A X. { B } ) : A --> C )
5 3 4 sylibr
 |-  ( B e. C -> ( A X. { B } ) e. ( C ^m A ) )