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

Metamath Proof Explorer

Theorem dmmptssf

Description: The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses dmmptssf.1 ⊢ Ⅎ _ x A
dmmptssf.2 ⊢ F = x ∈ A ⟼ B
Assertion dmmptssf ⊢ dom ⁡ F ⊆ A

Proof

Step Hyp Ref Expression
1 dmmptssf.1 ⊢ Ⅎ _ x A
2 dmmptssf.2 ⊢ F = x ∈ A ⟼ B
3 2 dmmpt ⊢ dom ⁡ F = x ∈ A | B ∈ V
4 1 ssrab2f ⊢ x ∈ A | B ∈ V ⊆ A
5 3 4 eqsstri ⊢ dom ⁡ F ⊆ A