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 } ) ) )