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

Theorem dmmptss 5308
Description: The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
Hypothesis
Ref Expression
dmmpt2.1  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
dmmptss  |-  dom  F  C_  A
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    F( x)

Proof of Theorem dmmptss
StepHypRef Expression
1 dmmpt2.1 . . 3  |-  F  =  ( x  e.  A  |->  B )
21dmmpt 5307 . 2  |-  dom  F  =  { x  e.  A  |  B  e.  _V }
3 ssrab2 3373 . 2  |-  { x  e.  A  |  B  e.  _V }  C_  A
42, 3eqsstri 3323 1  |-  dom  F  C_  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1717   {crab 2655   _Vcvv 2901    C_ wss 3265    e. cmpt 4209   dom cdm 4820
This theorem is referenced by:  fvmptss  5754  fvmptex  5756  fvmptnf  5763  mptexg  5906  dmmpt2ssx  6357  curry1val  6380  curry2val  6384  tposssxp  6421  mptfi  7343  bitsval  12865  subcrcl  13945  homarcl  14112  arwval  14127  arwrcl  14128  coafval  14148  submrcl  14676  issubg  14873  isnsg  14898  cntzrcl  15055  gsumconst  15461  gsumunsn  15473  issubrg  15797  abvrcl  15838  psrass1lem  16371  psrass1  16398  psrdi  16399  psrdir  16400  psrcom  16401  psrass23  16402  psropprmul  16561  coe1mul2  16591  isobs  16872  lmrcl  17219  1stcrestlem  17438  kgeni  17492  ptbasfi  17536  elmptrab  17782  isxms2  18370  setsmstopn  18400  tngtopn  18564  isphtpc  18892  pcofval  18908  cfili  19094  cfilfcls  19100  mpfrcl  19808  plybss  19982  ulmss  20182  dchrrcl  20893  issubgo  21741  mptct  23952  cvmsrcl  24732  snmlval  24799  islocfin  26069  eldiophb  26508  elmnc  27012  itgocn  27040  issdrg  27176
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156  df-opab 4210  df-mpt 4211  df-xp 4826  df-rel 4827  df-cnv 4828  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833
  Copyright terms: Public domain W3C validator