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 1536  dom cdm 5688  ⟶wf 6558

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 6565  df-f 6566

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  7105  dff3  7119  ffvresb  7144  dmfex  7927  fiun  7965  soseq  8182  fsuppeq  8198  fsuppeqg  8199  issmo2  8387  smoiso  8400  mapprc  8868  elpm2r  8883  map0b  8921  mapsnd  8924  brdomg  8995  brdomgOLD  8996  pw2f1olem  9114  iunmapdisj  10060  fodomfi2  10097  infmap2  10254  coftr  10310  fin23lem40  10388  isf34lem7  10416  axdc3lem2  10488  axdc3lem4  10490  rpnnen1lem4  13019  rpnnen1lem5  13020  fseqsupcl  14014  fseqsupubi  14015  ello12  15548  lo1bdd  15552  elo12  15559  o1bdd  15563  lo1o1  15564  rlimclim  15578  ramval  17041  0ram2  17054  0ramcl  17056  intopsn  18679  mndpsuppss  18790  symgfixf1  19469  f1omvdconj  19478  pmtrdifellem1  19508  pmtrdifellem2  19509  gsumval3  19939  dprdss  20063  dmdprdsplitlem  20071  ablfaclem3  20121  evpmss  21621  pjdm2  21748  islindf2  21851  islindf4  21875  decpmatval  22786  pmatcollpw3lem  22804  iscnp3  23267  cnpnei  23287  cncls2  23296  cncls  23297  cnntr  23298  cncnp  23303  cndis  23314  paste  23317  cncmp  23415  imacmp  23420  hauscmplem  23429  cnconn  23445  kgencn  23579  xkopt  23678  xkococnlem  23682  fbasrn  23907  fmval  23966  fmf  23968  rnelfmlem  23975  rnelfm  23976  cnflf2  24026  psmetdmdm  24330  xmetres  24389  metres  24390  metcnp  24569  metustsym  24583  cfilucfil  24587  metuel2  24593  iscauf  25327  equivcau  25347  lmclimf  25351  ismbf  25676  ismbfcn  25677  mbfimaicc  25679  mbfimaopn2  25705  ibl0  25836  cniccibl  25890  cnicciblnc  25892  dvnfre  26004  c1liplem1  26049  c1lip2  26051  dvcnvrelem2  26071  plyco0  26245  plyeq0  26264  vieta1lem2  26367  ulm2  26442  ulmss  26454  ulmdvlem2  26458  ulmdvlem3  26459  itgulm  26465  basellem5  27142  nodmon  27709  eedimeq  28927  axcontlem10  29002  wlkn0  29653  wlkres  29702  wlkp1lem1  29705  pthdivtx  29761  dmadjrnb  31934  elnlfn  31956  xppreima  32661  symgcom2  33086  tocyc01  33120  tocyccntz  33146  elrspunidl  33435  smatrcl  33756  mdetpmtr1  33783  locfinreflem  33800  hauseqcn  33858  rge0scvg  33909  indpreima  34005  isrnmeas  34180  omsfval  34275  omscl  34276  omsf  34277  eulerpartlemv  34345  eulerpartlemd  34347  eulerpartlemb  34349  eulerpartlemr  34355  eulerpartlemgvv  34357  eulerpartlemgs2  34361  eulerpartlemn  34362  rpsqrtcn  34586  cvmlift2lem9  35295  cvmlift3lem7  35309  mrsubfval  35492  ivthALT  36317  curf  37584  uncf  37585  unccur  37589  matunitlindflem2  37603  ptrecube  37606  heicant  37641  mbfresfi  37652  itg2addnclem  37657  itg2addnclem2  37658  ftc1anclem1  37679  indexdom  37720  sdclem2  37728  cnres2  37749  sstotbnd2  37760  bnd2lem  37777  ismgmOLD  37836  ismndo2  37860  exidreslem  37863  rngosn3  37910  rngodm1dm2  37918  rhmqusspan  42166  coeq0i  42740  pw2f1ocnv  43025  cnioobibld  43202  dfno2  43417  fresin2  45114  evthiccabs  45448  dvsubcncf  45879  dvmulcncf  45880  dvdivcncf  45882  cnbdibl  45917  fourierdlem48  46109  fourierdlem49  46110  fourierdlem58  46119  fourierdlem59  46120  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem80  46141  fourierdlem81  46142  fourierdlem89  46150  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem94  46155  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fouriercn  46187  sge0val  46321  fge0iccico  46325  isomennd  46486  3f1oss1  47024  fafv2elrnb  47184  fmtnoinf  47460  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  domnmsuppn0  48213  scmsuppss  48215  fdivmpt  48389  fdivmptf  48390  refdivmptf  48391  fdivpm  48392  refdivpm  48393  elbigo2  48401  elbigolo1  48406