Theorem fdm 6719

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 6709	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6644	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5663  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6543  df-f 6544

This theorem is used by:  fdmd  6720  fdmi  6721  fimacnv  6732  fssxp  6737  ffdm  6739  f00  6764  f0dom0  6766  f0rn0  6767  fimadmfo  6805  fimadmfoALT  6807  focofo  6809  feldmfvelcdm  7085  dff3  7099  ffvresb  7125  dmfex  7908  fiun  7946  soseq  8161  fsuppeq  8177  fsuppeqg  8178  issmo2  8342  smoiso  8355  mapprc  8834  elpm2r  8848  map0b  8887  mapsnd  8890  brdomg  8961  pw2f1olem  9076  iunmapdisj  10023  fodomfi2  10060  infmap2  10216  coftr  10272  fin23lem40  10350  isf34lem7  10378  axdc3lem2  10450  axdc3lem4  10452  rpnnen1lem4  13020  rpnnen1lem5  13021  fseqsupcl  14031  fseqsupubi  14032  ello12  15591  lo1bdd  15595  elo12  15602  o1bdd  15606  lo1o1  15607  rlimclim  15621  ramval  17090  0ram2  17103  0ramcl  17105  intopsn  18736  mndpsuppss  18860  symgfixf1  19551  f1omvdconj  19560  pmtrdifellem1  19590  pmtrdifellem2  19591  gsumval3  20021  dprdss  20145  dmdprdsplitlem  20153  ablfaclem3  20203  evpmss  21786  pjdm2  21911  islindf2  22014  islindf4  22038  decpmatval  22972  pmatcollpw3lem  22990  iscnp3  23451  cnpnei  23471  cncls2  23480  cncls  23481  cnntr  23482  cncnp  23487  cndis  23498  paste  23501  cncmp  23599  imacmp  23604  hauscmplem  23613  cnconn  23629  kgencn  23764  xkopt  23863  xkococnlem  23867  fbasrn  24092  fmval  24151  fmf  24153  rnelfmlem  24160  rnelfm  24161  cnflf2  24211  psmetdmdm  24513  xmetres  24572  metres  24573  metcnp  24749  metustsym  24763  cfilucfil  24767  metuel2  24773  iscauf  25490  equivcau  25510  lmclimf  25514  ismbf  25838  ismbfcn  25839  mbfimaicc  25841  mbfimaopn2  25867  ibl0  25997  cniccibl  26051  cnicciblnc  26053  dvnfre  26162  c1liplem1  26206  c1lip2  26208  dvcnvrelem2  26228  plyco0  26400  plyeq0  26419  vieta1lem2  26523  ulm2  26599  ulmss  26611  ulmdvlem2  26615  ulmdvlem3  26616  itgulm  26622  basellem5  27300  nodmon  27865  newbdayim  28147  eedimeq  29303  axcontlem10  29378  wlkn0  30028  wlkres  30076  wlkp1lem1  30079  pthdivtx  30139  cyclnumvtx  30215  dmadjrnb  32329  elnlfn  32351  xppreima  33061  indpreima  33255  symgcom2  33468  tocyc01  33502  tocyccntz  33528  elrspunidl  33800  smatrcl  34250  mdetpmtr1  34277  locfinreflem  34294  hauseqcn  34352  rge0scvg  34403  isrnmeas  34655  omsfval  34749  omscl  34750  omsf  34751  eulerpartlemv  34819  eulerpartlemd  34821  eulerpartlemb  34823  eulerpartlemr  34829  eulerpartlemgvv  34831  eulerpartlemgs2  34835  eulerpartlemn  34836  rpsqrtcn  35045  cvmlift2lem9  35840  cvmlift3lem7  35854  mrsubfval  36037  ivthALT  36903  curf  38306  uncf  38307  unccur  38311  matunitlindflem2  38325  ptrecube  38328  heicant  38363  mbfresfi  38374  itg2addnclem  38379  itg2addnclem2  38380  ftc1anclem1  38401  indexdom  38443  sdclem2  38451  cnres2  38472  sstotbnd2  38483  bnd2lem  38500  ismgmOLD  38559  ismndo2  38583  exidreslem  38586  rngosn3  38633  rngodm1dm2  38641  rhmqusspan  43010  coeq0i  43542  pw2f1ocnv  43822  cnioobibld  43999  dfno2  44212  fresin2  45948  evthiccabs  46270  dvsubcncf  46696  dvmulcncf  46697  dvdivcncf  46699  cnbdibl  46734  fourierdlem48  46926  fourierdlem49  46927  fourierdlem58  46936  fourierdlem59  46937  fourierdlem71  46949  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem80  46958  fourierdlem81  46959  fourierdlem89  46967  fourierdlem91  46969  fourierdlem92  46970  fourierdlem93  46971  fourierdlem94  46972  fourierdlem111  46989  fourierdlem112  46990  fourierdlem113  46991  fouriercn  47004  sge0val  47138  fge0iccico  47142  isomennd  47303  tannpoly  47685  3f1oss1  47870  fafv2elrnb  48030  fmtnoinf  48346  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  upgrimwlklem2  48721  upgrimwlklem3  48722  upgrimtrlslem2  48728  cycl3grtri  48770  domnmsuppn0  49206  scmsuppss  49208  fdivmpt  49377  fdivmptf  49378  refdivmptf  49379  fdivpm  49380  refdivpm  49381  elbigo2  49389  elbigolo1  49394  xpco2  49692