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

Theorem dmmptss 5486
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 5485 . 2  |-  dom  F  =  { x  e.  A  |  B  e.  _V }
3 ssrab2 3571 . 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 1398    e. wcel 1823   {crab 2808   _Vcvv 3106    C_ wss 3461    |-> cmpt 4497   dom cdm 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-mpt 4499  df-xp 4994  df-rel 4995  df-cnv 4996  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001
This theorem is referenced by:  mptrcl  5937  fvmptss  5940  fvmptex  5942  fvmptnf  5949  elfvmptrab1  5952  mptexg  6117  dmmpt2ssx  6838  curry1val  6866  curry2val  6870  tposssxp  6951  mptfi  7811  cnvimamptfin  7813  cantnfres  8087  bitsval  14158  subcrcl  15304  homarcl  15506  arwval  15521  arwrcl  15522  coafval  15542  submrcl  16176  issubg  16400  isnsg  16429  cntzrcl  16564  gsumconst  17152  issubrg  17624  abvrcl  17665  psrass1lem  18224  psrass1  18255  psrass23l  18258  psrcom  18259  psrass23  18260  mpfrcl  18382  psropprmul  18474  coe1mul2  18505  isobs  18924  lmrcl  19899  1stcrestlem  20119  islocfin  20184  kgeni  20204  ptbasfi  20248  elmptrab  20494  isxms2  21117  setsmstopn  21147  tngtopn  21330  isphtpc  21660  pcofval  21676  cfili  21873  cfilfcls  21879  rrxmval  21998  plybss  22757  ulmss  22958  dchrrcl  23713  issubgo  25503  mptct  27771  gsummpt2co  28005  locfinreflem  28078  sitgclg  28548  cvmsrcl  28973  snmlval  29040  eldiophb  30929  elmnc  31326  itgocn  31354  issdrg  31387  submgmrcl  32842  dmmpt2ssx2  33180
  Copyright terms: Public domain W3C validator