This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ A ⟼ B
Assertion mptiniseg ⊢ C ∈ V → F -1 C = x ∈ A | B = C

Proof

Step Hyp Ref Expression
1 dmmpt.1 ⊢ F = x ∈ A ⟼ B
2 1 mptpreima ⊢ F -1 C = x ∈ A | B ∈ C
3 elsn2g ⊢ C ∈ V → B ∈ C ↔ B = C
4 3 rabbidv ⊢ C ∈ V → x ∈ A | B ∈ C = x ∈ A | B = C
5 2 4 eqtrid ⊢ C ∈ V → F -1 C = x ∈ A | B = C