Theorem dmmptss

Description: The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013)

	Ref	Expression
Hypothesis	dmmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	dmmptss	⊢ dom 𝐹 ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	dmmpt	⊢ dom 𝐹 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
3	2	ssrab3	⊢ dom 𝐹 ⊆ 𝐴