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  39370  pw2f1ocnv  39654  cnioobibld  39840  fresin2  41448  evthiccabs  41791  dvsubcncf  42229  dvmulcncf  42230  dvdivcncf  42232  cnbdibl  42267  fourierdlem48  42459  fourierdlem49  42460  fourierdlem58  42469  fourierdlem59  42470  fourierdlem71  42482  fourierdlem73  42484  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem80  42491  fourierdlem81  42492  fourierdlem89  42500  fourierdlem91  42502  fourierdlem92  42503  fourierdlem93  42504  fourierdlem94  42505  fourierdlem111  42522  fourierdlem112  42523  fourierdlem113  42524  fouriercn  42537  sge0val  42668  fge0iccico  42672  isomennd  42833  fafv2elrnb  43454  fmtnoinf  43718  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  domnmsuppn0  44437  mndpsuppss  44439  scmsuppss  44440  fdivmpt  44620  fdivmptf  44621  refdivmptf  44622  fdivpm  44623  refdivpm  44624  elbigo2  44632  elbigolo1  44637