Theorem dmmptss 5793

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

Syntax hints:   = wceq 1632   ∈ wcel 2140  {crab 3055  Vcvv 3341   ⊆ wss 3716   ↦ cmpt 4882  dom cdm 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806  df-opab 4866  df-mpt 4883  df-xp 5273  df-rel 5274  df-cnv 5275  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280

This theorem is referenced by:  mptrcl  6453  fvmptss  6456  fvmptex  6458  fvmptnf  6466  elfvmptrab1  6469  mptexg  6650  dmmpt2ssx  7405  curry1val  7440  curry2val  7444  tposssxp  7527  mptfi  8433  cnvimamptfin  8435  cantnfres  8750  mptct  9573  bitsval  15369  subcrcl  16698  arwval  16915  arwrcl  16916  coafval  16936  submrcl  17568  issubg  17816  isnsg  17845  cntzrcl  17981  gsumconst  18555  abvrcl  19044  psrass1lem  19600  psrass1  19628  psrass23l  19631  psrcom  19632  psrass23  19633  mpfrcl  19741  psropprmul  19831  coe1mul2  19862  isobs  20287  lmrcl  21258  1stcrestlem  21478  islocfin  21543  kgeni  21563  ptbasfi  21607  isxms2  22475  setsmstopn  22505  tngtopn  22676  isphtpc  23015  pcofval  23031  cfili  23287  cfilfcls  23293  rrxmval  23409  plybss  24170  ulmss  24371  dchrrcl  25186  gsummpt2co  30111  locfinreflem  30238  sitgclg  30735  cvmsrcl  31575  snmlval  31642  eldiophb  37841  elmnc  38227  itgocn  38255  issdrg  38288  submgmrcl  42311  dmmpt2ssx2  42644