Theorem dmmptss 5631

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

Syntax hints:   = wceq 1483   ∈ wcel 1990  {crab 2916  Vcvv 3200   ⊆ wss 3574   ↦ cmpt 4729  dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  mptrcl  6289  fvmptss  6292  fvmptex  6294  fvmptnf  6302  elfvmptrab1  6305  mptexg  6484  dmmpt2ssx  7235  curry1val  7270  curry2val  7274  tposssxp  7356  mptfi  8265  cnvimamptfin  8267  cantnfres  8574  mptct  9360  bitsval  15146  subcrcl  16476  arwval  16693  arwrcl  16694  coafval  16714  submrcl  17346  issubg  17594  isnsg  17623  cntzrcl  17760  gsumconst  18334  abvrcl  18821  psrass1lem  19377  psrass1  19405  psrass23l  19408  psrcom  19409  psrass23  19410  mpfrcl  19518  psropprmul  19608  coe1mul2  19639  isobs  20064  lmrcl  21035  1stcrestlem  21255  islocfin  21320  kgeni  21340  ptbasfi  21384  isxms2  22253  setsmstopn  22283  tngtopn  22454  isphtpc  22793  pcofval  22810  cfili  23066  cfilfcls  23072  rrxmval  23188  plybss  23950  ulmss  24151  dchrrcl  24965  gsummpt2co  29780  locfinreflem  29907  sitgclg  30404  cvmsrcl  31246  snmlval  31313  eldiophb  37320  elmnc  37706  itgocn  37734  issdrg  37767  submgmrcl  41782  dmmpt2ssx2  42115