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

Metamath Proof Explorer

Theorem dmmpti

Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses fnmpti.1 ⊢ B ∈ V
fnmpti.2 ⊢ F = x ∈ A ⟼ B
Assertion dmmpti ⊢ dom ⁡ F = A

Proof

Step Hyp Ref Expression
1 fnmpti.1 ⊢ B ∈ V
2 fnmpti.2 ⊢ F = x ∈ A ⟼ B
3 1 2 fnmpti ⊢ F Fn A
4 3 fndmi ⊢ dom ⁡ F = A