Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmmptss Structured version   Visualization version   GIF version

Theorem dmmptss 6066
 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
StepHypRef Expression
1 dmmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
21dmmpt 6065 . 2 dom 𝐹 = {𝑥𝐴𝐵 ∈ V}
32ssrab3 4011 1 dom 𝐹𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∈ wcel 2112  Vcvv 3444   ⊆ wss 3884   ↦ cmpt 5113  dom cdm 5523 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-mpt 5114  df-xp 5529  df-rel 5530  df-cnv 5531  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536 This theorem is referenced by:  mptrcl  6758  fvmptss  6761  fvmptex  6763  fvmptnf  6771  elfvmptrab1w  6775  elfvmptrab1  6776  mptexg  6965  mptexw  7640  dmmpossx  7750  tposssxp  7883  mptfi  8811  cnvimamptfin  8813  cantnfres  9128  mptct  9953  arwrcl  17299  cntzrcl  18452  gsumconst  19050  psrass1lem  20618  psrass1  20646  psrass23l  20649  psrcom  20650  psrass23  20651  mpfrcl  20760  psropprmul  20870  coe1mul2  20901  lmrcl  21839  1stcrestlem  22060  ptbasfi  22189  isxms2  23058  setsmstopn  23088  tngtopn  23259  rrxmval  24012  ulmss  24995  dchrrcl  25827  gsummpt2co  30736  locfinreflem  31193  sitgclg  31708  cvmsrcl  32619  snmlval  32686  gonan0  32747  bj-fvmptunsn1  34667  eldiophb  39685  elmnc  40067  itgocn  40095  submgmrcl  44389  dmmpossx2  44725
 Copyright terms: Public domain W3C validator