Theorem dmmptss 6197

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3438   ⊆ wss 3899   ↦ cmpt 5177  dom cdm 5622

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-xp 5628  df-rel 5629  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  mptrcl  6948  fvmptss  6951  fvmptex  6953  fvmptnf  6961  elfvmptrab1w  6966  elfvmptrab1  6967  mptexg  7165  mptexw  7895  dmmpossx  8008  tposssxp  8170  mptfi  9249  cnvimamptfin  9251  cantnfres  9584  mptct  10446  arwrcl  17966  submgmrcl  18618  cntzrcl  19254  gsumconst  19861  psrass1lem  21886  psrass1  21917  psrass23l  21920  psrcom  21921  psrass23  21922  mpfrcl  22038  psropprmul  22176  coe1mul2  22209  lmrcl  23173  1stcrestlem  23394  ptbasfi  23523  isxms2  24390  setsmstopn  24420  tngtopn  24592  rrxmval  25359  ulmss  26360  dchrrcl  27205  gsummpt2co  33080  locfinreflem  33946  sitgclg  34448  cvmsrcl  35407  snmlval  35474  gonan0  35535  bj-fvmptunsn1  37401  eldiophb  42941  elmnc  43320  itgocn  43348  tannpoly  47078  dmmpossx2  48525  dmtposss  49063