Theorem dmmptss 6199

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 6198	. 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3	2	ssrab3 4034	1 ⊢ dom 𝐹 ⊆ 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901   ↦ cmpt 5179  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  mptrcl  6950  fvmptss  6953  fvmptex  6955  fvmptnf  6963  elfvmptrab1w  6968  elfvmptrab1  6969  mptexg  7167  mptexw  7897  dmmpossx  8010  tposssxp  8172  mptfi  9251  cnvimamptfin  9253  cantnfres  9586  mptct  10448  arwrcl  17968  submgmrcl  18620  cntzrcl  19256  gsumconst  19863  psrass1lem  21888  psrass1  21919  psrass23l  21922  psrcom  21923  psrass23  21924  mpfrcl  22040  psropprmul  22178  coe1mul2  22211  lmrcl  23175  1stcrestlem  23396  ptbasfi  23525  isxms2  24392  setsmstopn  24422  tngtopn  24594  rrxmval  25361  ulmss  26362  dchrrcl  27207  gsummpt2co  33131  locfinreflem  33997  sitgclg  34499  cvmsrcl  35458  snmlval  35525  gonan0  35586  bj-fvmptunsn1  37462  eldiophb  42999  elmnc  43378  itgocn  43406  tannpoly  47136  dmmpossx2  48583  dmtposss  49121