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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	mptiniseg	⊢ ( 𝐶 ∈ 𝑉 → ( ◡ 𝐹 “ { 𝐶 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	mptpreima	⊢ ( ◡ 𝐹 “ { 𝐶 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { 𝐶 } }
3		elsn2g	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐵 ∈ { 𝐶 } ↔ 𝐵 = 𝐶 ) )
4	3	rabbidv	⊢ ( 𝐶 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { 𝐶 } } = { 𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶 } )
5	2 4	eqtrid	⊢ ( 𝐶 ∈ 𝑉 → ( ◡ 𝐹 “ { 𝐶 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶 } )