Theorem fnimaeq0

Description: Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 . (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Assertion	fnimaeq0	|- ( ( F Fn A /\ B C_ A ) -> ( ( F " B ) = (/) <-> B = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		imadisj	|- ( ( F " B ) = (/) <-> ( dom F i^i B ) = (/) )
2		incom	|- ( dom F i^i B ) = ( B i^i dom F )
3		fndm	|- ( F Fn A -> dom F = A )
4	3	sseq2d	|- ( F Fn A -> ( B C_ dom F <-> B C_ A ) )
5	4	biimpar	|- ( ( F Fn A /\ B C_ A ) -> B C_ dom F )
6		df-ss	|- ( B C_ dom F <-> ( B i^i dom F ) = B )
7	5 6	sylib	|- ( ( F Fn A /\ B C_ A ) -> ( B i^i dom F ) = B )
8	2 7	eqtrid	|- ( ( F Fn A /\ B C_ A ) -> ( dom F i^i B ) = B )
9	8	eqeq1d	|- ( ( F Fn A /\ B C_ A ) -> ( ( dom F i^i B ) = (/) <-> B = (/) ) )
10	1 9	bitrid	|- ( ( F Fn A /\ B C_ A ) -> ( ( F " B ) = (/) <-> B = (/) ) )