Theorem dmmptss 6228

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

Syntax hints:   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904   ↦ cmpt 5181  dom cdm 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5653  df-rel 5654  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660

This theorem is referenced by:  mptrcl  6985  fvmptss  6988  fvmptex  6990  fvmptnf  6998  elfvmptrab1w  7003  elfvmptrab1  7004  mptexg  7205  mptexw  7934  dmmpossx  8047  tposssxp  8210  mptfi  9294  cnvimamptfin  9296  cantnfres  9632  mptct  10495  arwrcl  18077  submgmrcl  18729  cntzrcl  19367  gsumconst  19974  psrass1lem  21985  psrass1  22015  psrass23l  22018  psrcom  22019  psrass23  22020  mpfrcl  22138  psropprmul  22299  coe1mul2  22332  lmrcl  23291  1stcrestlem  23512  ptbasfi  23641  isxms2  24508  setsmstopn  24538  tngtopn  24710  rrxmval  25467  ulmss  26460  dchrrcl  27304  gsummpt2co  33228  locfinreflem  34137  sitgclg  34639  cvmsrcl  35614  snmlval  35681  gonan0  35742  bj-fvmptunsn1  37749  eldiophb  43338  elmnc  43713  itgocn  43741  tannpoly  47484  dmmpossx2  48959  dmtposss  49497