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

Theorem fdm 6267
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 6259 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 6204 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  dom cdm 5318   Fn wfn 6099  wf 6100
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 198  df-an 385  df-fn 6107  df-f 6108
This theorem is referenced by:  fdmd  6268  fdmi  6269  fssxp  6278  ffdm  6280  f00  6305  f0dom0  6307  f0rn0  6308  foco  6344  fimacnv  6572  dff3  6597  ffvresb  6619  dmfex  7357  frnsuppeq  7544  suppss  7563  issmo2  7685  smoiso  7698  mapprc  8099  elpm2r  8113  map0b  8135  mapsnd  8137  brdomg  8205  pw2f1olem  8306  iunmapdisj  9132  fodomfi2  9169  infmap2  9328  coftr  9383  fin23lem40  9461  isf34lem7  9489  axdc3lem2  9561  axdc3lem4  9563  rpnnen1lem4  12039  rpnnen1lem5  12040  fseqsupcl  13003  fseqsupubi  13004  ello12  14473  lo1bdd  14477  elo12  14484  o1bdd  14488  lo1o1  14489  rlimclim  14503  ramval  15932  0ram2  15945  0ramcl  15947  intopsn  17461  symgfixf1  18061  f1omvdconj  18070  pmtrdifellem1  18100  pmtrdifellem2  18101  gsumval3  18512  dprdss  18633  dmdprdsplitlem  18641  ablfaclem3  18691  evpmss  20142  pjdm2  20269  islindf2  20367  islindf4  20391  decpmatval  20787  pmatcollpw3lem  20805  iscnp3  21266  cnpnei  21286  cncls2  21295  cncls  21296  cnntr  21297  cncnp  21302  cndis  21313  paste  21316  cncmp  21413  imacmp  21418  hauscmplem  21427  cnconn  21443  kgencn  21577  xkopt  21676  xkococnlem  21680  fbasrn  21905  fmval  21964  fmf  21966  rnelfmlem  21973  rnelfm  21974  cnflf2  22024  psmetdmdm  22327  xmetres  22386  metres  22387  metcnp  22563  metustsym  22577  cfilucfil  22581  metuel2  22587  iscauf  23295  equivcau  23315  lmclimf  23319  ismbf  23615  ismbfcn  23616  mbfimaicc  23618  mbfimaopn2  23644  ibl0  23773  cniccibl  23827  dvnfre  23935  c1liplem1  23979  c1lip2  23981  dvcnvrelem2  24001  plyco0  24168  plyeq0  24187  vieta1lem2  24286  ulm2  24359  ulmss  24371  ulmdvlem2  24375  ulmdvlem3  24376  itgulm  24382  basellem5  25031  tgcgr4  25646  eedimeq  25998  axcontlem10  26073  wlkn0  26750  wlkres  26801  wlkp1lem1  26804  pthdivtx  26859  dmadjrnb  29099  elnlfn  29121  xppreima  29782  smatrcl  30193  mdetpmtr1  30220  locfinreflem  30238  hauseqcn  30272  rge0scvg  30326  indpreima  30418  isrnmeas  30594  omsfval  30687  omscl  30688  omsf  30689  eulerpartlemv  30757  eulerpartlemd  30759  eulerpartlemb  30761  eulerpartlemr  30767  eulerpartlemgvv  30769  eulerpartlemgs2  30773  eulerpartlemn  30774  rpsqrtcn  31002  cvmlift2lem9  31621  cvmlift3lem7  31635  mrsubfval  31733  soseq  32080  nodmon  32129  ivthALT  32656  curf  33702  uncf  33703  unccur  33707  matunitlindflem2  33721  ptrecube  33724  heicant  33759  mbfresfi  33770  itg2addnclem  33775  itg2addnclem2  33776  cnicciblnc  33795  ftc1anclem1  33799  indexdom  33843  sdclem2  33851  cnres2  33875  sstotbnd2  33886  bnd2lem  33903  ismgmOLD  33962  ismndo2  33986  exidreslem  33989  rngosn3  34036  rngodm1dm2  34044  coeq0i  37819  pw2f1ocnv  38106  cnioobibld  38300  fresin2  39842  evthiccabs  40203  dvsubcncf  40620  dvmulcncf  40621  dvdivcncf  40623  cnbdibl  40658  fourierdlem48  40851  fourierdlem49  40852  fourierdlem58  40861  fourierdlem59  40862  fourierdlem71  40874  fourierdlem73  40876  fourierdlem74  40877  fourierdlem75  40878  fourierdlem76  40879  fourierdlem80  40883  fourierdlem81  40884  fourierdlem89  40892  fourierdlem91  40894  fourierdlem92  40895  fourierdlem93  40896  fourierdlem94  40897  fourierdlem111  40914  fourierdlem112  40915  fourierdlem113  40916  fouriercn  40929  sge0val  41063  fge0iccico  41067  isomennd  41228  fafv2elrnb  41825  fmtnoinf  42024  nnsum4primeseven  42264  nnsum4primesevenALTV  42265  domnmsuppn0  42719  mndpsuppss  42721  scmsuppss  42722  fdivmpt  42903  fdivmptf  42904  refdivmptf  42905  fdivpm  42906  refdivpm  42907  elbigo2  42915  elbigolo1  42920
  Copyright terms: Public domain W3C validator