Theorem dmmptss 6205

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889   ↦ cmpt 5166  dom cdm 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  mptrcl  6957  fvmptss  6960  fvmptex  6962  fvmptnf  6970  elfvmptrab1w  6975  elfvmptrab1  6976  mptexg  7176  mptexw  7906  dmmpossx  8019  tposssxp  8180  mptfi  9261  cnvimamptfin  9263  cantnfres  9598  mptct  10460  arwrcl  18011  submgmrcl  18663  cntzrcl  19302  gsumconst  19909  psrass1lem  21912  psrass1  21942  psrass23l  21945  psrcom  21946  psrass23  21947  mpfrcl  22063  psropprmul  22201  coe1mul2  22234  lmrcl  23196  1stcrestlem  23417  ptbasfi  23546  isxms2  24413  setsmstopn  24443  tngtopn  24615  rrxmval  25372  ulmss  26362  dchrrcl  27203  gsummpt2co  33109  locfinreflem  33984  sitgclg  34486  cvmsrcl  35446  snmlval  35513  gonan0  35574  bj-fvmptunsn1  37571  eldiophb  43189  elmnc  43564  itgocn  43592  tannpoly  47338  dmmpossx2  48813  dmtposss  49351