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

Metamath Proof Explorer

Theorem dmmpt

Description: The domain of the mapping operation in general. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 22-Mar-2015)

Ref Expression
Hypothesis dmmpt.1 ⊢ F = x ∈ A ⟼ B
Assertion dmmpt ⊢ dom ⁡ F = x ∈ A | B ∈ V

Proof

Step Hyp Ref Expression
1 dmmpt.1 ⊢ F = x ∈ A ⟼ B
2 dfdm4 ⊢ dom ⁡ F = ran ⁡ F -1
3 dfrn4 ⊢ ran ⁡ F -1 = F -1 V
4 1 mptpreima ⊢ F -1 V = x ∈ A | B ∈ V
5 2 3 4 3eqtri ⊢ dom ⁡ F = x ∈ A | B ∈ V