Theorem fdmd 6679

Description: Deduction form of fdm 6678. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
fdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
fdmd	⊢ (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fdmd

Step	Hyp	Ref	Expression
1		fdmd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fdm 6678	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5631  ⟶wf 6495

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 6502  df-f 6503

This theorem is referenced by:  fssdmd  6687  fssdm  6688  foima  6758  focnvimacdmdm  6765  resdif  6802  fssrescdmd  7080  fmptco  7083  funfvima2d  7187  focdmex  7909  suppsnop  8128  onnseq  8284  fopwdom  9023  fodomfib  9239  fodomfibOLD  9241  intrnfi  9329  ordtypelem5  9437  ordtypelem6  9438  ordtypelem7  9439  ordtypelem8  9440  brwdomn0  9484  wdomtr  9490  fseqenlem2  9947  fin23lem30  10264  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  fin1a2lem7  10328  ttukeylem6  10436  fodomb  10448  pwxpndom2  10588  hashf1lem1  14417  wrddm  14483  ccatdmss  14544  swrdcl  14608  cats1un  14683  repswswrd  14746  limsupgle  15439  limsupgre  15443  rlim  15457  rlimi  15475  lo1o1  15494  rlimuni  15512  o1co  15548  rlimcn1  15550  ruclem11  16207  1arith  16898  ramval  16979  0ram  16991  mrcuni  17587  homarcl2  18002  prfval  18165  pfxchn  18576  chnind  18587  chnccats1  18591  chnccat  18592  gsumval  18645  gsumval2  18654  mndpsuppss  18733  frmdss2  18831  ghmrn  19204  cntzmhm2  19317  gsumval3  19882  gsumzaddlem  19896  dmdprdd  19976  dprdres  20005  dprdf1  20010  dprd2da  20019  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dmdprdsplit  20024  dprdsplit  20025  dpjidcl  20035  ablfac1eulem  20049  ablfac1eu  20050  ablfaclem2  20063  ablfac2  20066  lmhmlsp  21044  rhmpreimaidl  21275  frlmsslsp  21776  f1lindf  21802  mattpostpos  22419  iinopn  22867  lmbrf  23225  cnntri  23236  cnclsi  23237  lmcnp  23269  cnt0  23311  cnt1  23315  cnhaus  23319  cncmp  23357  connima  23390  1stcfb  23410  1stccnp  23427  1stckgenlem  23518  kgencn3  23523  txcnpi  23573  txcnp  23585  prdstps  23594  xkohaus  23618  xkoco2cn  23623  qtopeu  23681  hmeores  23736  fmfnfmlem2  23920  fmfnfmlem4  23922  fmfnfm  23923  lmflf  23970  txflf  23971  cnextfval  24027  cnextcn  24032  clssubg  24074  ghmcnp  24080  qustgplem  24086  tsmsval  24096  ucncn  24249  xmetdmdm  24300  metn0  24325  tmsval  24446  metustid  24519  metustexhalf  24521  metustfbas  24522  isngp2  24562  evth  24926  lmmbrf  25229  iscfil2  25233  caufval  25242  iscau2  25244  caucfil  25250  ovollb2  25456  ovolunlem1a  25463  ovoliunlem1  25469  ovoliun2  25473  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem6  25555  mbfconstlem  25594  ismbfcn  25596  mbfmulc2lem  25614  mbfmulc2re  25615  cncombf  25625  mbfaddlem  25627  mbflimsup  25633  i1f0rn  25649  itg1addlem5  25667  itg1climres  25681  mbfmullem2  25691  limcfval  25839  limcdif  25843  ellimc2  25844  ellimc3  25846  limccnp  25858  dvfval  25864  cpnord  25902  cpnres  25904  dvcmul  25911  dvcmulf  25912  dvexp  25920  dvgt0lem1  25969  dvcnvrelem1  25984  itgpowd  26017  plyaddlem1  26178  plymullem1  26179  plycpn  26255  aalioulem3  26300  tayl0  26327  dvntaylp  26336  ulm2  26350  ulmdvlem1  26365  xrlimcnp  26932  dchrelbas2  27200  dchrghm  27219  dchrptlem1  27227  dchrptlem2  27228  iscgrgd  28581  iscgrglt  28582  trgcgrg  28583  tgcgr4  28599  motcgrg  28612  wrdupgr  29154  wrdumgr  29166  grporndm  30581  sspn  30807  fmptcof2  32730  fnpreimac  32743  curry2ima  32782  fpwrelmap  32806  indf1ofs  32926  swrdf1  33016  pmtrcnel  33150  pmtrcnel2  33151  pmtrcnelor  33152  wrdpmtrlast  33154  cycpmcl  33177  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem1  33187  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cyc3co2  33201  cycpmconjv  33203  fxpgaval  33228  rmfsupp2  33299  elrgspnsubrunlem2  33309  rndrhmcl  33357  elrspunidl  33488  rhmimaidl  33492  1arithidomlem2  33596  1arithidom  33597  evls1dm  33621  evlextv  33686  esplymhp  33712  esplysply  33715  esplyfval1  33717  ply1degltdimlem  33766  fldextrspunlsp  33818  irngnzply1lem  33834  irngnzply1  33835  zarcmplem  34025  rhmpreimacnlem  34028  esumpcvgval  34222  ofcfval4  34249  measdivcst  34368  oms0  34441  omsmon  34442  omssubaddlem  34443  omssubadd  34444  carsgval  34447  omsmeas  34467  sitgclg  34486  eulerpartlemgu  34521  sseqfv2  34538  rrvdm  34590  ftc2re  34742  cvmliftmolem1  35463  cvmliftlem3  35469  cvmliftlem10  35476  cvmliftlem13  35478  cvmlift2lem9  35493  cvmlift3lem6  35506  cvmlift3lem7  35507  mclsax  35751  mclsppslem  35765  mclspps  35766  fwddifval  36344  fwddifnval  36345  weiunfrlem  36646  bj-finsumval0  37599  curunc  37923  itg2addnclem2  37993  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem8  38021  sdclem2  38063  isbnd3  38105  ssbnd  38109  bnd2lem  38112  ismtyval  38121  grpokerinj  38214  rngosn3  38245  rngodm1dm2  38253  divrngcl  38278  isdrngo2  38279  sticksstones1  42585  aks5lem2  42626  evlselvlem  43019  mapfzcons2  43151  fnwe2lem2  43479  lmhmfgima  43512  wnefimgd  44588  binomcxplemnotnn0  44783  cncmpmax  45463  mullimcf  46053  limsuppnfdlem  46129  limsupvaluz  46136  climxrrelem  46177  climxrre  46178  liminfvalxr  46211  liminflimsupxrre  46245  xlimmnfvlem2  46261  xlimpnfvlem2  46265  xlimliminflimsup  46290  cncfuni  46314  cncficcgt0  46316  cncfioobd  46325  dvsinax  46341  itgperiod  46409  fvvolioof  46417  fvvolicof  46419  stoweidlem29  46457  fourierdlem20  46555  fourierdlem53  46587  fourierdlem63  46597  fourierdlem68  46602  fourierdlem82  46616  sge0sn  46807  sge0tsms  46808  sge0cl  46809  sge0isum  46855  ismeannd  46895  hoicvr  46976  dmovn  47032  hspmbl  47057  ovolval4lem1  47077  ovnovollem1  47084  ovnovollem2  47085  issmfd  47163  issmfdf  47165  cnfsmf  47168  issmfled  47185  issmfgtd  47189  smfsuplem1  47239  smfdivdmmbl2  47269  fcores  47509  f1cof1blem  47516  f1cof1b  47519  funfocofob  47520  rmsuppss  48840  itcovalendof  49139  ffvbr  49325  lmdran  50140  cmdlan  50141