Theorem mptiniseg

Description: Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Hypothesis	dmmpt.1	|- F = ( x e. A |-> B )
Assertion	mptiniseg	|- ( C e. V -> ( `' F " { C } ) = { x e. A | B = C } )

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	|- F = ( x e. A |-> B )
2	1	mptpreima	|- ( `' F " { C } ) = { x e. A | B e. { C } }
3		elsn2g	|- ( C e. V -> ( B e. { C } <-> B = C ) )
4	3	rabbidv	|- ( C e. V -> { x e. A | B e. { C } } = { x e. A | B = C } )
5	2 4	eqtrid	|- ( C e. V -> ( `' F " { C } ) = { x e. A | B = C } )