Theorem dmmptss 5590

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 5589	. 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		ssrab2 3666	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⊆ 𝐴
4	2, 3	eqsstri 3614	1 ⊢ dom 𝐹 ⊆ 𝐴

Syntax hints:   = wceq 1480   ∈ wcel 1987  {crab 2911  Vcvv 3186   ⊆ wss 3555   ↦ cmpt 4673  dom cdm 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-mpt 4675  df-xp 5080  df-rel 5081  df-cnv 5082  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087

This theorem is referenced by:  mptrcl  6246  fvmptss  6249  fvmptex  6251  fvmptnf  6258  elfvmptrab1  6261  mptexg  6438  dmmpt2ssx  7180  curry1val  7215  curry2val  7219  tposssxp  7301  mptfi  8209  cnvimamptfin  8211  cantnfres  8518  mptct  9304  bitsval  15070  subcrcl  16397  arwval  16614  arwrcl  16615  coafval  16635  submrcl  17267  issubg  17515  isnsg  17544  cntzrcl  17681  gsumconst  18255  abvrcl  18742  psrass1lem  19296  psrass1  19324  psrass23l  19327  psrcom  19328  psrass23  19329  mpfrcl  19437  psropprmul  19527  coe1mul2  19558  isobs  19983  lmrcl  20945  1stcrestlem  21165  islocfin  21230  kgeni  21250  ptbasfi  21294  isxms2  22163  setsmstopn  22193  tngtopn  22364  isphtpc  22701  pcofval  22718  cfili  22974  cfilfcls  22980  rrxmval  23096  plybss  23854  ulmss  24055  dchrrcl  24865  gsummpt2co  29562  locfinreflem  29686  sitgclg  30182  cvmsrcl  30951  snmlval  31018  eldiophb  36797  elmnc  37184  itgocn  37212  issdrg  37245  submgmrcl  41067  dmmpt2ssx2  41400