Theorem fdm 6522

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 6514	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 6455	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5555   Fn wfn 6350  ⟶wf 6351

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 209  df-an 399  df-fn 6358  df-f 6359

This theorem is referenced by:  fdmd  6523  fdmi  6524  fssxp  6534  ffdm  6536  f00  6561  f0dom0  6563  f0rn0  6564  fimadmfo  6599  fimadmfoALT  6601  foco  6602  fimacnv  6839  dff3  6866  ffvresb  6888  dmfex  7641  fiun  7644  frnsuppeq  7842  suppss  7860  issmo2  7986  smoiso  7999  mapprc  8410  elpm2r  8424  map0b  8447  mapsnd  8450  brdomg  8519  pw2f1olem  8621  iunmapdisj  9449  fodomfi2  9486  infmap2  9640  coftr  9695  fin23lem40  9773  isf34lem7  9801  axdc3lem2  9873  axdc3lem4  9875  rpnnen1lem4  12380  rpnnen1lem5  12381  fseqsupcl  13346  fseqsupubi  13347  ello12  14873  lo1bdd  14877  elo12  14884  o1bdd  14888  lo1o1  14889  rlimclim  14903  ramval  16344  0ram2  16357  0ramcl  16359  intopsn  17864  symgfixf1  18565  f1omvdconj  18574  pmtrdifellem1  18604  pmtrdifellem2  18605  gsumval3  19027  dprdss  19151  dmdprdsplitlem  19159  ablfaclem3  19209  evpmss  20730  pjdm2  20855  islindf2  20958  islindf4  20982  decpmatval  21373  pmatcollpw3lem  21391  iscnp3  21852  cnpnei  21872  cncls2  21881  cncls  21882  cnntr  21883  cncnp  21888  cndis  21899  paste  21902  cncmp  22000  imacmp  22005  hauscmplem  22014  cnconn  22030  kgencn  22164  xkopt  22263  xkococnlem  22267  fbasrn  22492  fmval  22551  fmf  22553  rnelfmlem  22560  rnelfm  22561  cnflf2  22611  psmetdmdm  22915  xmetres  22974  metres  22975  metcnp  23151  metustsym  23165  cfilucfil  23169  metuel2  23175  iscauf  23883  equivcau  23903  lmclimf  23907  ismbf  24229  ismbfcn  24230  mbfimaicc  24232  mbfimaopn2  24258  ibl0  24387  cniccibl  24441  dvnfre  24549  c1liplem1  24593  c1lip2  24595  dvcnvrelem2  24615  plyco0  24782  plyeq0  24801  vieta1lem2  24900  ulm2  24973  ulmss  24985  ulmdvlem2  24989  ulmdvlem3  24990  itgulm  24996  basellem5  25662  eedimeq  26684  axcontlem10  26759  wlkn0  27402  wlkres  27452  wlkp1lem1  27455  pthdivtx  27510  dmadjrnb  29683  elnlfn  29705  xppreima  30394  symgcom2  30728  tocyc01  30760  tocyccntz  30786  smatrcl  31061  mdetpmtr1  31088  locfinreflem  31104  hauseqcn  31138  rge0scvg  31192  indpreima  31284  isrnmeas  31459  omsfval  31552  omscl  31553  omsf  31554  eulerpartlemv  31622  eulerpartlemd  31624  eulerpartlemb  31626  eulerpartlemr  31632  eulerpartlemgvv  31634  eulerpartlemgs2  31638  eulerpartlemn  31639  rpsqrtcn  31864  cvmlift2lem9  32558  cvmlift3lem7  32572  mrsubfval  32755  soseq  33096  nodmon  33157  ivthALT  33683  curf  34885  uncf  34886  unccur  34890  matunitlindflem2  34904  ptrecube  34907  heicant  34942  mbfresfi  34953  itg2addnclem  34958  itg2addnclem2  34959  cnicciblnc  34978  ftc1anclem1  34982  indexdom  35024  sdclem2  35032  cnres2  35056  sstotbnd2  35067  bnd2lem  35084  ismgmOLD  35143  ismndo2  35167  exidreslem  35170  rngosn3  35217  rngodm1dm2  35225  coeq0i  39399  pw2f1ocnv  39683  cnioobibld  39869  fresin2  41477  evthiccabs  41820  dvsubcncf  42258  dvmulcncf  42259  dvdivcncf  42261  cnbdibl  42296  fourierdlem48  42488  fourierdlem49  42489  fourierdlem58  42498  fourierdlem59  42499  fourierdlem71  42511  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem80  42520  fourierdlem81  42521  fourierdlem89  42529  fourierdlem91  42531  fourierdlem92  42532  fourierdlem93  42533  fourierdlem94  42534  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fouriercn  42566  sge0val  42697  fge0iccico  42701  isomennd  42862  fafv2elrnb  43483  fmtnoinf  43747  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  domnmsuppn0  44466  mndpsuppss  44468  scmsuppss  44469  fdivmpt  44649  fdivmptf  44650  refdivmptf  44651  fdivpm  44652  refdivpm  44653  elbigo2  44661  elbigolo1  44666