Metamath Proof Explorer

Theorem fconst6g

Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion fconst6g 
|- ( B e. C -> ( A X. { B } ) : A --> C )

Proof

Step Hyp Ref Expression
1 fconstg 
 |-  ( B e. C -> ( A X. { B } ) : A --> { B } )
2 snssi 
 |-  ( B e. C -> { B } C_ C )
3 1 2 fssd 
 |-  ( B e. C -> ( A X. { B } ) : A --> C )