Theorem fdmd 6717

Description: Deduction form of fdm 6716. 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 6716	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5659  ⟶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:  fssdmd  6725  fssdm  6726  foima  6798  focnvimacdmdm  6805  resdif  6843  fssrescdmd  7124  fmptco  7127  funfvima2d  7235  focdmex  7957  suppsnop  8180  onnseq  8337  fopwdom  9087  fodomfib  9302  intrnfi  9390  ordtypelem5  9498  ordtypelem6  9499  ordtypelem7  9500  ordtypelem8  9501  brwdomn0  9545  wdomtr  9551  fseqenlem2  10032  fin23lem30  10348  isf34lem5  10384  isf34lem7  10385  isf34lem6  10386  fin1a2lem7  10412  ttukeylem6  10520  fodomb  10533  pwxpndom2  10678  hashf1lem1  14524  wrddm  14590  ccatdmss  14651  swrdcl  14717  swrdf1  14723  cats1un  14794  repswswrd  14859  limsupgle  15568  limsupgre  15572  rlim  15586  rlimi  15604  lo1o1  15623  rlimuni  15641  o1co  15677  rlimcn1  15679  ruclem11  16334  1arith  17025  ramval  17106  0ram  17118  mrcuni  17715  homarcl2  18130  prfval  18293  pfxchn  18704  chnind  18715  chnccats1  18719  chnccat  18720  gsumval  18785  gsumval2  18794  mndpsuppss  18878  frmdss2  18978  ghmrn  19362  cntzmhm2  19475  gsumval3  20040  gsumzaddlem  20054  dmdprdd  20134  dprdres  20163  dprdf1  20168  dprd2da  20177  dmdprdsplit2lem  20180  dmdprdsplit2  20181  dmdprdsplit  20182  dprdsplit  20183  dpjidcl  20193  ablfac1eulem  20207  ablfac1eu  20208  ablfaclem2  20221  ablfac2  20224  crngrhmfo  20643  lmhmlsp  21239  rhmpreimaidl  21485  frlmsslsp  22015  f1lindf  22041  mattpostpos  22682  iinopn  23133  lmbrf  23491  cnntri  23502  cnclsi  23503  lmcnp  23535  cnt0  23577  cnt1  23581  cnhaus  23585  cncmp  23623  connima  23656  1stcfb  23676  1stccnp  23694  1stckgenlem  23785  kgencn3  23790  txcnpi  23840  txcnp  23852  prdstps  23861  xkohaus  23885  xkoco2cn  23890  qtopeu  23948  hmeores  24003  fmfnfmlem2  24187  fmfnfmlem4  24189  fmfnfm  24190  lmflf  24237  txflf  24238  cnextfval  24294  cnextcn  24299  clssubg  24341  ghmcnp  24347  qustgplem  24353  tsmsval  24363  ucncn  24516  xmetdmdm  24567  metn0  24592  tmsval  24713  metustid  24786  metustexhalf  24788  metustfbas  24789  isngp2  24829  evth  25193  lmmbrf  25496  iscfil2  25500  caufval  25509  iscau2  25511  caucfil  25517  ovollb2  25723  ovolunlem1a  25730  ovoliunlem1  25736  ovoliun2  25740  ioombl1lem4  25795  uniioombllem1  25815  uniioombllem2  25817  uniioombllem6  25822  mbfconstlem  25861  ismbfcn  25863  mbfmulc2lem  25881  mbfmulc2re  25882  cncombf  25892  mbfaddlem  25894  mbflimsup  25900  i1f0rn  25916  itg1addlem5  25934  itg1climres  25948  mbfmullem2  25958  limcfval  26106  limcdif  26110  ellimc2  26111  ellimc3  26113  limccnp  26125  dvfval  26131  cpnord  26169  cpnres  26171  dvcmul  26178  dvcmulf  26179  dvexp  26187  dvgt0lem1  26236  dvcnvrelem1  26251  itgpowd  26284  plyaddlem1  26446  plymullem1  26447  plycpn  26526  rnplynfin  26546  plyconz  26547  aalioulem3  26577  tayl0  26605  dvntaylp  26614  ulm2  26628  ulmdvlem1  26643  xrlimcnp  27213  dchrelbas2  27481  dchrghm  27500  dchrptlem1  27508  dchrptlem2  27509  iscgrgd  28863  iscgrglt  28864  trgcgrg  28865  tgcgr4  28881  motcgrg  28894  wrdupgr  29550  wrdumgr  29562  grporndm  30999  sspn  31225  fmptcof2  33138  fnpreimac  33151  curry2ima  33189  fpwrelmap  33212  indf1ofs  33320  pmtrcnel  33537  pmtrcnel2  33538  pmtrcnelor  33539  wrdpmtrlast  33541  cycpmcl  33564  cycpmco2f1  33572  cycpmco2rn  33573  cycpmco2lem1  33574  cycpmco2lem2  33575  cycpmco2lem3  33576  cycpmco2lem4  33577  cycpmco2lem5  33578  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmco2  33581  cyc3co2  33588  cycpmconjv  33590  fxpgaval  33615  rmfsupp2  33685  elrgspnsubrunlem2  33696  rndrhmcl  33745  elrspunidl  33864  rhmimaidl  33868  1arithidomlem2  33954  1arithidom  33955  evls1dm  33979  selvascl  34035  evlextv  34060  esplymhp  34086  esplysply  34089  esplyfval1  34091  ply1degltdimlem  34140  fldextrspunlsp  34192  irngnzply1lem  34208  irngnzply1  34209  zarcmplem  34399  rhmpreimacnlem  34402  esumpcvgval  34596  ofcfval4  34623  measdivcst  34743  oms0  34816  omsmon  34817  omssubaddlem  34818  omssubadd  34819  carsgval  34822  omsmeas  34842  sitgclg  34861  eulerpartlemgu  34896  sseqfv2  34913  rrvdm  34965  ftc2re  35114  cvmliftmolem1  35868  cvmliftlem3  35874  cvmliftlem10  35881  cvmliftlem13  35883  cvmlift2lem9  35898  cvmlift3lem6  35911  cvmlift3lem7  35912  mclsax  36156  mclsppslem  36170  mclspps  36171  fwddifval  36750  fwddifnval  36751  weiunfrlem  37091  bj-finsumval0  38045  curunc  38364  itg2addnclem2  38429  ftc1anclem5  38454  ftc1anclem6  38455  ftc1anclem8  38457  sdclem2  38500  isbnd3  38542  ssbnd  38546  bnd2lem  38549  ismtyval  38558  grpokerinj  38651  rngosn3  38682  rngodm1dm2  38690  divrngcl  38715  isdrngo2  38716  sticksstones1  43020  aks5lem2  43061  evlselvlem  43442  mapfzcons2  43572  fnwe2lem2  43900  lmhmfgima  43933  wnefimgd  45009  binomcxplemnotnn0  45188  cncmpmax  45874  mullimcf  46461  limsuppnfdlem  46537  limsupvaluz  46544  climxrrelem  46585  climxrre  46586  liminfvalxr  46619  liminflimsupxrre  46653  xlimmnfvlem2  46669  xlimpnfvlem2  46673  xlimliminflimsup  46698  cncfuni  46722  cncficcgt0  46724  cncfioobd  46733  dvsinax  46749  itgperiod  46817  fvvolioof  46825  fvvolicof  46827  stoweidlem29  46865  fourierdlem20  46963  fourierdlem48  46990  fourierdlem49  46991  fourierdlem53  46995  fourierdlem63  47005  fourierdlem68  47010  fourierdlem82  47024  fourierdlem113  47055  sge0sn  47215  sge0tsms  47216  sge0cl  47217  sge0isum  47263  ismeannd  47303  hoicvr  47384  dmovn  47440  hspmbl  47465  ovolval4lem1  47485  ovnovollem1  47492  ovnovollem2  47493  issmfd  47571  issmfdf  47573  cnfsmf  47576  issmfled  47593  issmfgtd  47597  smfsuplem1  47647  smfdivdmmbl2  47677  tmachlem-agreesn  47783  fcores  47963  f1cof1blem  47970  f1cof1b  47973  funfocofob  47974  rmsuppss  49308  itcovalendof  49607  ffvbr  49792  lmdran  50605  cmdlan  50606