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

Metamath Proof Explorer

Theorem dmmptif

Description: Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses dmmptif.1 ⊢ Ⅎ _ x A
dmmptif.2 ⊢ B ∈ V
dmmptif.3 ⊢ F = x ∈ A ⟼ B
Assertion dmmptif ⊢ dom ⁡ F = A

Proof

Step Hyp Ref Expression
1 dmmptif.1 ⊢ Ⅎ _ x A
2 dmmptif.2 ⊢ B ∈ V
3 dmmptif.3 ⊢ F = x ∈ A ⟼ B
4 1 2 3 fnmptif ⊢ F Fn A
5 fndm ⊢ F Fn A → dom ⁡ F = A
6 4 5 ax-mp ⊢ dom ⁡ F = A