Theorem dmmptss 5548

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

Hypothesis

Ref	Expression
dmmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
dmmptss	⊢ dom 𝐹 ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem dmmptss

Step	Hyp	Ref	Expression
1		dmmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 5547	. 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		ssrab2 3650	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⊆ 𝐴
4	2, 3	eqsstri 3598	1 ⊢ dom 𝐹 ⊆ 𝐴

Syntax hints:   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173   ⊆ wss 3540   ↦ cmpt 4643  dom cdm 5038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  mptrcl  6198  fvmptss  6201  fvmptex  6203  fvmptnf  6210  elfvmptrab1  6213  mptexg  6389  dmmpt2ssx  7124  curry1val  7157  curry2val  7161  tposssxp  7243  mptfi  8148  cnvimamptfin  8150  cantnfres  8457  bitsval  14984  subcrcl  16299  arwval  16516  arwrcl  16517  coafval  16537  submrcl  17169  issubg  17417  isnsg  17446  cntzrcl  17583  gsumconst  18157  abvrcl  18644  psrass1lem  19198  psrass1  19226  psrass23l  19229  psrcom  19230  psrass23  19231  mpfrcl  19339  psropprmul  19429  coe1mul2  19460  isobs  19883  lmrcl  20845  1stcrestlem  21065  islocfin  21130  kgeni  21150  ptbasfi  21194  isxms2  22063  setsmstopn  22093  tngtopn  22264  isphtpc  22601  pcofval  22618  cfili  22874  cfilfcls  22880  rrxmval  22996  plybss  23754  ulmss  23955  dchrrcl  24765  mptct  28880  gsummpt2co  29111  locfinreflem  29235  sitgclg  29731  cvmsrcl  30500  snmlval  30567  eldiophb  36338  elmnc  36725  itgocn  36753  issdrg  36786  submgmrcl  41572  dmmpt2ssx2  41908