Theorem i1fima2sn

Description: Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Assertion	i1fima2sn	|- ( ( F e. dom S.1 /\ A e. ( B \ { 0 } ) ) -> ( vol ` ( `' F " { A } ) ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		eldifn	|- ( A e. ( B \ { 0 } ) -> -. A e. { 0 } )
2		elsni	|- ( 0 e. { A } -> 0 = A )
3		snidg	|- ( 0 e. { A } -> 0 e. { 0 } )
4	2 3	eqeltrrd	|- ( 0 e. { A } -> A e. { 0 } )
5	1 4	nsyl	|- ( A e. ( B \ { 0 } ) -> -. 0 e. { A } )
6		i1fima2	|- ( ( F e. dom S.1 /\ -. 0 e. { A } ) -> ( vol ` ( `' F " { A } ) ) e. RR )
7	5 6	sylan2	|- ( ( F e. dom S.1 /\ A e. ( B \ { 0 } ) ) -> ( vol ` ( `' F " { A } ) ) e. RR )