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=\left(x\in A⟼B\right)$$
Assertion	mptiniseg	$$⊢C\in V\to F^{-1}\left[\left\{C\right\}\right]=\left\{x\in A|B=C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2	1	mptpreima	$$⊢F^{-1}\left[\left\{C\right\}\right]=\left\{x\in A|B\in \left\{C\right\}\right\}$$
3		elsn2g	$$⊢C\in V\to \left(B\in \left\{C\right\}\leftrightarrow B=C\right)$$
4	3	rabbidv	$$⊢C\in V\to \left\{x\in A|B\in \left\{C\right\}\right\}=\left\{x\in A|B=C\right\}$$
5	2 4	eqtrid	$$⊢C\in V\to F^{-1}\left[\left\{C\right\}\right]=\left\{x\in A|B=C\right\}$$