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

Proof

Step	Hyp	Ref	Expression
1		dmmptssf.1	⊢ Ⅎ 𝑥 𝐴
2		dmmptssf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	2	dmmpt	⊢ dom 𝐹 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
4	1	ssrab2f	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ 𝐴
5	3 4	eqsstri	⊢ dom 𝐹 ⊆ 𝐴