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 ⊢ Ⅎ 𝑥 𝐴
dmmptif.2 ⊢ 𝐵 ∈ V
dmmptif.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion dmmptif dom 𝐹 = 𝐴

Proof

Step Hyp Ref Expression
1 dmmptif.1 ⊢ Ⅎ 𝑥 𝐴
2 dmmptif.2 ⊢ 𝐵 ∈ V
3 dmmptif.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 1 2 3 fnmptif ⊢ 𝐹 Fn 𝐴
5 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6 4 5 ax-mp ⊢ dom 𝐹 = 𝐴