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

Theorem fdm 6516
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 6508 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 6449 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  dom cdm 5549   Fn wfn 6344  wf 6345
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 208  df-an 397  df-fn 6352  df-f 6353
This theorem is referenced by:  fdmd  6517  fdmi  6518  fssxp  6528  ffdm  6530  f00  6555  f0dom0  6557  f0rn0  6558  fimadmfo  6593  fimadmfoALT  6595  foco  6596  fimacnv  6832  dff3  6859  ffvresb  6881  dmfex  7629  fiunw  7632  fiun  7635  frnsuppeq  7833  suppss  7851  issmo2  7977  smoiso  7990  mapprc  8400  elpm2r  8414  map0b  8437  mapsnd  8439  brdomg  8508  pw2f1olem  8610  iunmapdisj  9438  fodomfi2  9475  infmap2  9629  coftr  9684  fin23lem40  9762  isf34lem7  9790  axdc3lem2  9862  axdc3lem4  9864  rpnnen1lem4  12369  rpnnen1lem5  12370  fseqsupcl  13335  fseqsupubi  13336  ello12  14863  lo1bdd  14867  elo12  14874  o1bdd  14878  lo1o1  14879  rlimclim  14893  ramval  16334  0ram2  16347  0ramcl  16349  intopsn  17854  symgfixf1  18496  f1omvdconj  18505  pmtrdifellem1  18535  pmtrdifellem2  18536  gsumval3  18958  dprdss  19082  dmdprdsplitlem  19090  ablfaclem3  19140  evpmss  20660  pjdm2  20785  islindf2  20888  islindf4  20912  decpmatval  21303  pmatcollpw3lem  21321  iscnp3  21782  cnpnei  21802  cncls2  21811  cncls  21812  cnntr  21813  cncnp  21818  cndis  21829  paste  21832  cncmp  21930  imacmp  21935  hauscmplem  21944  cnconn  21960  kgencn  22094  xkopt  22193  xkococnlem  22197  fbasrn  22422  fmval  22481  fmf  22483  rnelfmlem  22490  rnelfm  22491  cnflf2  22541  psmetdmdm  22844  xmetres  22903  metres  22904  metcnp  23080  metustsym  23094  cfilucfil  23098  metuel2  23104  iscauf  23812  equivcau  23832  lmclimf  23836  ismbf  24158  ismbfcn  24159  mbfimaicc  24161  mbfimaopn2  24187  ibl0  24316  cniccibl  24370  dvnfre  24478  c1liplem1  24522  c1lip2  24524  dvcnvrelem2  24544  plyco0  24711  plyeq0  24730  vieta1lem2  24829  ulm2  24902  ulmss  24914  ulmdvlem2  24918  ulmdvlem3  24919  itgulm  24925  basellem5  25590  eedimeq  26612  axcontlem10  26687  wlkn0  27330  wlkres  27380  wlkp1lem1  27383  pthdivtx  27438  dmadjrnb  29611  elnlfn  29633  xppreima  30323  symgcom2  30656  tocyc01  30688  tocyccntz  30714  smatrcl  30961  mdetpmtr1  30988  locfinreflem  31004  hauseqcn  31038  rge0scvg  31092  indpreima  31184  isrnmeas  31359  omsfval  31452  omscl  31453  omsf  31454  eulerpartlemv  31522  eulerpartlemd  31524  eulerpartlemb  31526  eulerpartlemr  31532  eulerpartlemgvv  31534  eulerpartlemgs2  31538  eulerpartlemn  31539  rpsqrtcn  31764  cvmlift2lem9  32456  cvmlift3lem7  32470  mrsubfval  32653  soseq  32994  nodmon  33055  ivthALT  33581  curf  34752  uncf  34753  unccur  34757  matunitlindflem2  34771  ptrecube  34774  heicant  34809  mbfresfi  34820  itg2addnclem  34825  itg2addnclem2  34826  cnicciblnc  34845  ftc1anclem1  34849  indexdom  34892  sdclem2  34900  cnres2  34924  sstotbnd2  34935  bnd2lem  34952  ismgmOLD  35011  ismndo2  35035  exidreslem  35038  rngosn3  35085  rngodm1dm2  35093  coeq0i  39230  pw2f1ocnv  39514  cnioobibld  39700  fresin2  41308  evthiccabs  41651  dvsubcncf  42089  dvmulcncf  42090  dvdivcncf  42092  cnbdibl  42127  fourierdlem48  42320  fourierdlem49  42321  fourierdlem58  42330  fourierdlem59  42331  fourierdlem71  42343  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem80  42352  fourierdlem81  42353  fourierdlem89  42361  fourierdlem91  42363  fourierdlem92  42364  fourierdlem93  42365  fourierdlem94  42366  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fouriercn  42398  sge0val  42529  fge0iccico  42533  isomennd  42694  fafv2elrnb  43315  fmtnoinf  43545  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  domnmsuppn0  44315  mndpsuppss  44317  scmsuppss  44318  fdivmpt  44498  fdivmptf  44499  refdivmptf  44500  fdivpm  44501  refdivpm  44502  elbigo2  44510  elbigolo1  44515
  Copyright terms: Public domain W3C validator