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

Theorem fdm 6495
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm
StepHypRef Expression
1 ffn 6487 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 6428 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  dom cdm 5528   Fn wfn 6323  wf 6324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400  df-fn 6331  df-f 6332
This theorem is referenced by:  fdmd  6496  fdmi  6497  fssxp  6507  ffdm  6509  f00  6534  f0dom0  6536  f0rn0  6537  fimadmfo  6572  fimadmfoALT  6574  foco  6575  fimacnv  6812  dff3  6839  ffvresb  6861  dmfex  7616  fiun  7619  frnsuppeq  7817  suppss  7835  issmo2  7961  smoiso  7974  mapprc  8385  elpm2r  8399  map0b  8422  mapsnd  8425  brdomg  8494  pw2f1olem  8596  iunmapdisj  9426  fodomfi2  9463  infmap2  9617  coftr  9672  fin23lem40  9750  isf34lem7  9778  axdc3lem2  9850  axdc3lem4  9852  rpnnen1lem4  12357  rpnnen1lem5  12358  fseqsupcl  13328  fseqsupubi  13329  ello12  14852  lo1bdd  14856  elo12  14863  o1bdd  14867  lo1o1  14868  rlimclim  14882  ramval  16321  0ram2  16334  0ramcl  16336  intopsn  17842  symgfixf1  18543  f1omvdconj  18552  pmtrdifellem1  18582  pmtrdifellem2  18583  gsumval3  19005  dprdss  19129  dmdprdsplitlem  19137  ablfaclem3  19187  evpmss  20705  pjdm2  20830  islindf2  20933  islindf4  20957  decpmatval  21348  pmatcollpw3lem  21366  iscnp3  21827  cnpnei  21847  cncls2  21856  cncls  21857  cnntr  21858  cncnp  21863  cndis  21874  paste  21877  cncmp  21975  imacmp  21980  hauscmplem  21989  cnconn  22005  kgencn  22139  xkopt  22238  xkococnlem  22242  fbasrn  22467  fmval  22526  fmf  22528  rnelfmlem  22535  rnelfm  22536  cnflf2  22586  psmetdmdm  22890  xmetres  22949  metres  22950  metcnp  23126  metustsym  23140  cfilucfil  23144  metuel2  23150  iscauf  23862  equivcau  23882  lmclimf  23886  ismbf  24210  ismbfcn  24211  mbfimaicc  24213  mbfimaopn2  24239  ibl0  24368  cniccibl  24422  cnicciblnc  24424  dvnfre  24533  c1liplem1  24577  c1lip2  24579  dvcnvrelem2  24599  plyco0  24767  plyeq0  24786  vieta1lem2  24885  ulm2  24958  ulmss  24970  ulmdvlem2  24974  ulmdvlem3  24975  itgulm  24981  basellem5  25648  eedimeq  26670  axcontlem10  26745  wlkn0  27388  wlkres  27438  wlkp1lem1  27441  pthdivtx  27496  dmadjrnb  29667  elnlfn  29689  xppreima  30380  symgcom2  30735  tocyc01  30767  tocyccntz  30793  smatrcl  31071  mdetpmtr1  31098  locfinreflem  31114  hauseqcn  31148  rge0scvg  31199  indpreima  31291  isrnmeas  31466  omsfval  31559  omscl  31560  omsf  31561  eulerpartlemv  31629  eulerpartlemd  31631  eulerpartlemb  31633  eulerpartlemr  31639  eulerpartlemgvv  31641  eulerpartlemgs2  31645  eulerpartlemn  31646  rpsqrtcn  31871  cvmlift2lem9  32565  cvmlift3lem7  32579  mrsubfval  32762  soseq  33103  nodmon  33164  ivthALT  33690  curf  34915  uncf  34916  unccur  34920  matunitlindflem2  34934  ptrecube  34937  heicant  34972  mbfresfi  34983  itg2addnclem  34988  itg2addnclem2  34989  ftc1anclem1  35010  indexdom  35052  sdclem2  35060  cnres2  35081  sstotbnd2  35092  bnd2lem  35109  ismgmOLD  35168  ismndo2  35192  exidreslem  35195  rngosn3  35242  rngodm1dm2  35250  coeq0i  39491  pw2f1ocnv  39775  cnioobibld  39961  fresin2  41584  evthiccabs  41926  dvsubcncf  42359  dvmulcncf  42360  dvdivcncf  42362  cnbdibl  42397  fourierdlem48  42589  fourierdlem49  42590  fourierdlem58  42599  fourierdlem59  42600  fourierdlem71  42612  fourierdlem73  42614  fourierdlem74  42615  fourierdlem75  42616  fourierdlem76  42617  fourierdlem80  42621  fourierdlem81  42622  fourierdlem89  42630  fourierdlem91  42632  fourierdlem92  42633  fourierdlem93  42634  fourierdlem94  42635  fourierdlem111  42652  fourierdlem112  42653  fourierdlem113  42654  fouriercn  42667  sge0val  42798  fge0iccico  42802  isomennd  42963  fafv2elrnb  43584  fmtnoinf  43846  nnsum4primeseven  44112  nnsum4primesevenALTV  44113  domnmsuppn0  44564  mndpsuppss  44566  scmsuppss  44567  fdivmpt  44747  fdivmptf  44748  refdivmptf  44749  fdivpm  44750  refdivpm  44751  elbigo2  44759  elbigolo1  44764
  Copyright terms: Public domain W3C validator