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

Theorem dmmptss 5493
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 5492 . 2  |-  dom  F  =  { x  e.  A  |  B  e.  _V }
3 ssrab2 3570 . 2  |-  { x  e.  A  |  B  e.  _V }  C_  A
42, 3eqsstri 3519 1  |-  dom  F  C_  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    e. wcel 1804   {crab 2797   _Vcvv 3095    C_ wss 3461    |-> cmpt 4495   dom cdm 4989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-mpt 4497  df-xp 4995  df-rel 4996  df-cnv 4997  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002
This theorem is referenced by:  fvmptss  5949  fvmptex  5951  fvmptnf  5958  elfvmptrab1  5961  mptexg  6127  dmmpt2ssx  6850  curry1val  6878  curry2val  6882  tposssxp  6961  mptfi  7821  cnvimamptfin  7823  cantnfres  8099  bitsval  13951  subcrcl  15062  homarcl  15229  arwval  15244  arwrcl  15245  coafval  15265  submrcl  15851  issubg  16075  isnsg  16104  cntzrcl  16239  gsumconst  16828  issubrg  17303  abvrcl  17344  psrass1lem  17903  psrass1  17934  psrass23l  17937  psrcom  17938  psrass23  17939  mpfrcl  18061  psropprmul  18153  coe1mul2  18184  isobs  18624  lmrcl  19605  1stcrestlem  19826  islocfin  19891  kgeni  19911  ptbasfi  19955  elmptrab  20201  isxms2  20824  setsmstopn  20854  tngtopn  21037  isphtpc  21367  pcofval  21383  cfili  21580  cfilfcls  21586  rrxmval  21705  plybss  22464  ulmss  22664  dchrrcl  23387  issubgo  25177  mptct  27413  gsummpt2co  27644  locfinreflem  27716  sitgclg  28157  cvmsrcl  28582  snmlval  28649  eldiophb  30665  elmnc  31061  itgocn  31089  issdrg  31122  submgmrcl  32308  dmmpt2ssx2  32659
  Copyright terms: Public domain W3C validator