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 F /\ A C_ dom F ) -> ( A. x e. A ( F ` x ) = B <-> A C_ ( `' F " { B } ) ) )

Proof

Step Hyp Ref Expression
1 funimass4 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ { B } <-> A. x e. A ( F ` x ) e. { B } ) )
2 fvex 
 |-  ( F ` x ) e. _V
3 2 elsn 
 |-  ( ( F ` x ) e. { B } <-> ( F ` x ) = B )
4 3 ralbii 
 |-  ( A. x e. A ( F ` x ) e. { B } <-> A. x e. A ( F ` x ) = B )
5 1 4 bitr2di 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( A. x e. A ( F ` x ) = B <-> ( F " A ) C_ { B } ) )
6 funimass3 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ { B } <-> A C_ ( `' F " { B } ) ) )
7 5 6 bitrd 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( A. x e. A ( F ` x ) = B <-> A C_ ( `' F " { B } ) ) )