Theorem fdm 6745

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 29-May-2024.)

Assertion

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

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 6736	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6673	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685  ⟶wf 6557

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 207  df-an 396  df-fn 6564  df-f 6565

This theorem is referenced by:  fdmd  6746  fdmi  6747  fimacnv  6758  fssxp  6763  ffdm  6765  f00  6790  f0dom0  6792  f0rn0  6793  fimadmfo  6829  fimadmfoALT  6831  focofo  6833  feldmfvelcdm  7106  dff3  7120  ffvresb  7145  dmfex  7927  fiun  7967  soseq  8184  fsuppeq  8200  fsuppeqg  8201  issmo2  8389  smoiso  8402  mapprc  8870  elpm2r  8885  map0b  8923  mapsnd  8926  brdomg  8997  brdomgOLD  8998  pw2f1olem  9116  iunmapdisj  10063  fodomfi2  10100  infmap2  10257  coftr  10313  fin23lem40  10391  isf34lem7  10419  axdc3lem2  10491  axdc3lem4  10493  rpnnen1lem4  13022  rpnnen1lem5  13023  fseqsupcl  14018  fseqsupubi  14019  ello12  15552  lo1bdd  15556  elo12  15563  o1bdd  15567  lo1o1  15568  rlimclim  15582  ramval  17046  0ram2  17059  0ramcl  17061  intopsn  18667  mndpsuppss  18778  symgfixf1  19455  f1omvdconj  19464  pmtrdifellem1  19494  pmtrdifellem2  19495  gsumval3  19925  dprdss  20049  dmdprdsplitlem  20057  ablfaclem3  20107  evpmss  21604  pjdm2  21731  islindf2  21834  islindf4  21858  decpmatval  22771  pmatcollpw3lem  22789  iscnp3  23252  cnpnei  23272  cncls2  23281  cncls  23282  cnntr  23283  cncnp  23288  cndis  23299  paste  23302  cncmp  23400  imacmp  23405  hauscmplem  23414  cnconn  23430  kgencn  23564  xkopt  23663  xkococnlem  23667  fbasrn  23892  fmval  23951  fmf  23953  rnelfmlem  23960  rnelfm  23961  cnflf2  24011  psmetdmdm  24315  xmetres  24374  metres  24375  metcnp  24554  metustsym  24568  cfilucfil  24572  metuel2  24578  iscauf  25314  equivcau  25334  lmclimf  25338  ismbf  25663  ismbfcn  25664  mbfimaicc  25666  mbfimaopn2  25692  ibl0  25822  cniccibl  25876  cnicciblnc  25878  dvnfre  25990  c1liplem1  26035  c1lip2  26037  dvcnvrelem2  26057  plyco0  26231  plyeq0  26250  vieta1lem2  26353  ulm2  26428  ulmss  26440  ulmdvlem2  26444  ulmdvlem3  26445  itgulm  26451  basellem5  27128  nodmon  27695  eedimeq  28913  axcontlem10  28988  wlkn0  29639  wlkres  29688  wlkp1lem1  29691  pthdivtx  29747  cyclnumvtx  29820  dmadjrnb  31925  elnlfn  31947  xppreima  32655  indpreima  32850  symgcom2  33104  tocyc01  33138  tocyccntz  33164  elrspunidl  33456  smatrcl  33795  mdetpmtr1  33822  locfinreflem  33839  hauseqcn  33897  rge0scvg  33948  isrnmeas  34201  omsfval  34296  omscl  34297  omsf  34298  eulerpartlemv  34366  eulerpartlemd  34368  eulerpartlemb  34370  eulerpartlemr  34376  eulerpartlemgvv  34378  eulerpartlemgs2  34382  eulerpartlemn  34383  rpsqrtcn  34608  cvmlift2lem9  35316  cvmlift3lem7  35330  mrsubfval  35513  ivthALT  36336  curf  37605  uncf  37606  unccur  37610  matunitlindflem2  37624  ptrecube  37627  heicant  37662  mbfresfi  37673  itg2addnclem  37678  itg2addnclem2  37679  ftc1anclem1  37700  indexdom  37741  sdclem2  37749  cnres2  37770  sstotbnd2  37781  bnd2lem  37798  ismgmOLD  37857  ismndo2  37881  exidreslem  37884  rngosn3  37931  rngodm1dm2  37939  rhmqusspan  42186  coeq0i  42764  pw2f1ocnv  43049  cnioobibld  43226  dfno2  43441  fresin2  45177  evthiccabs  45509  dvsubcncf  45939  dvmulcncf  45940  dvdivcncf  45942  cnbdibl  45977  fourierdlem48  46169  fourierdlem49  46170  fourierdlem58  46179  fourierdlem59  46180  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem80  46201  fourierdlem81  46202  fourierdlem89  46210  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem94  46215  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fouriercn  46247  sge0val  46381  fge0iccico  46385  isomennd  46546  3f1oss1  47087  fafv2elrnb  47247  fmtnoinf  47523  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  cycl3grtri  47914  domnmsuppn0  48285  scmsuppss  48287  fdivmpt  48461  fdivmptf  48462  refdivmptf  48463  fdivpm  48464  refdivpm  48465  elbigo2  48473  elbigolo1  48478