Theorem fdm 6717

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

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

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 6540  df-f 6541

This theorem is used by:  fdmd  6718  fdmi  6719  fimacnv  6730  fssxp  6735  ffdm  6737  f00  6762  f0dom0  6764  f0rn0  6765  fimadmfo  6803  fimadmfoALT  6805  focofo  6807  feldmfvelcdm  7084  dff3  7098  ffvresb  7124  dmfex  7915  fiun  7953  soseq  8169  fsuppeq  8185  fsuppeqg  8186  issmo2  8350  smoiso  8363  mapprc  8844  elpm2r  8858  curf  8883  uncf  8884  map0b  8904  mapsnd  8907  brdomg  8978  pw2f1olem  9093  iunmapdisj  10095  fodomfi2  10132  infmap2  10288  coftr  10344  fin23lem40  10422  isf34lem7  10450  axdc3lem2  10522  axdc3lem4  10524  rpnnen1lem4  13101  rpnnen1lem5  13102  fseqsupcl  14113  fseqsupubi  14114  ello12  15676  lo1bdd  15680  elo12  15687  o1bdd  15691  lo1o1  15692  rlimclim  15706  ramval  17179  0ram2  17192  0ramcl  17194  intopsn  18825  mndpsuppss  18952  symgfixf1  19644  f1omvdconj  19653  pmtrdifellem1  19683  pmtrdifellem2  19684  gsumval3  20114  dprdss  20238  dmdprdsplitlem  20246  ablfaclem3  20296  evpmss  21885  pjdm2  22010  islindf2  22113  islindf4  22137  matunitlindflem2  22988  decpmatval  23076  pmatcollpw3lem  23094  iscnp3  23555  cnpnei  23575  cncls2  23584  cncls  23585  cnntr  23586  cncnp  23591  cndis  23602  paste  23605  cncmp  23703  imacmp  23708  hauscmplem  23717  cnconn  23733  kgencn  23868  xkopt  23967  xkococnlem  23971  fbasrn  24196  fmval  24255  fmf  24257  rnelfmlem  24264  rnelfm  24265  cnflf2  24315  psmetdmdm  24617  xmetres  24676  metres  24677  metcnp  24853  metustsym  24867  cfilucfil  24871  metuel2  24877  iscauf  25594  equivcau  25614  lmclimf  25618  ismbf  25942  ismbfcn  25943  mbfimaicc  25945  mbfimaopn2  25971  ibl0  26100  cniccibl  26154  cnicciblnc  26156  dvnfre  26265  c1liplem1  26309  c1lip2  26311  dvcnvrelem2  26331  plyco0  26503  plyeq0  26523  vieta1lem2  26627  ulm2  26705  ulmss  26717  ulmdvlem2  26721  ulmdvlem3  26722  itgulm  26728  basellem5  27405  nodmon  28000  newbdayim  28282  eedimeq  29469  axcontlem10  29544  wlkn0  30194  wlkres  30242  wlkp1lem1  30245  pthdivtx  30305  cyclnumvtx  30381  dmadjrnb  32501  elnlfn  32523  xppreima  33232  indpreima  33425  symgcom2  33638  tocyc01  33672  tocyccntz  33698  elrspunidl  33971  smatrcl  34421  mdetpmtr1  34448  locfinreflem  34465  hauseqcn  34523  rge0scvg  34574  isrnmeas  34826  omsfval  34919  omscl  34920  omsf  34921  eulerpartlemv  34989  eulerpartlemd  34991  eulerpartlemb  34993  eulerpartlemr  34999  eulerpartlemgvv  35001  eulerpartlemgs2  35005  eulerpartlemn  35006  rpsqrtcn  35215  cvmlift2lem9  36055  cvmlift3lem7  36069  mrsubfval  36252  ivthALT  37103  unccur  38506  ptrecube  38518  heicant  38553  mbfresfi  38564  itg2addnclem  38569  itg2addnclem2  38570  ftc1anclem1  38591  indexdom  38648  sdclem2  38656  cnres2  38677  sstotbnd2  38688  bnd2lem  38705  ismgmOLD  38764  ismndo2  38788  exidreslem  38791  rngosn3  38838  rngodm1dm2  38846  rhmqusspan  43215  coeq0i  43743  pw2f1ocnv  44023  cnioobibld  44200  dfno2  44413  fresin2  46156  evthiccabs  46477  dvsubcncf  46903  dvmulcncf  46904  dvdivcncf  46906  cnbdibl  46941  fourierdlem48  47133  fourierdlem49  47134  fourierdlem58  47143  fourierdlem59  47144  fourierdlem71  47156  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem80  47165  fourierdlem81  47166  fourierdlem89  47174  fourierdlem91  47176  fourierdlem92  47177  fourierdlem93  47178  fourierdlem94  47179  fourierdlem111  47196  fourierdlem112  47197  fourierdlem113  47198  fouriercn  47211  sge0val  47345  fge0iccico  47349  isomennd  47510  tannpoly  47909  3f1oss1  48114  fafv2elrnb  48274  fmtnoinf  48590  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  upgrimwlklem2  48965  upgrimwlklem3  48966  upgrimtrlslem2  48972  cycl3grtri  49014  domnmsuppn0  49450  scmsuppss  49452  fdivmpt  49621  fdivmptf  49622  refdivmptf  49623  fdivpm  49624  refdivpm  49625  elbigo2  49633  elbigolo1  49638  xpco2  49936