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

Metamath Proof Explorer

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 𝐹 ⊆ 𝐴