Theorem fdmd 6729

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677  ⟶wf 6540

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 206  df-an 398  df-fn 6547  df-f 6548

This theorem is referenced by:  fssdmd  6737  fssdm  6738  foima  6811  focnvimacdmdm  6818  resdif  6855  fmptco  7127  funfvima2d  7234  focdmex  7942  suppsnop  8163  onnseq  8344  fopwdom  9080  fodomfib  9326  intrnfi  9411  ordtypelem5  9517  ordtypelem6  9518  ordtypelem7  9519  ordtypelem8  9520  brwdomn0  9564  wdomtr  9570  fseqenlem2  10020  fin23lem30  10337  isf34lem5  10373  isf34lem7  10374  isf34lem6  10375  fin1a2lem7  10401  ttukeylem6  10509  fodomb  10521  pwxpndom2  10660  hashf1lem1  14415  hashf1lem1OLD  14416  wrddm  14471  swrdcl  14595  cats1un  14671  repswswrd  14734  limsupgle  15421  limsupgre  15425  rlim  15439  rlimi  15457  lo1o1  15476  rlimuni  15494  o1co  15530  rlimcn1  15532  ruclem11  16183  1arith  16860  ramval  16941  0ram  16953  mrcuni  17565  homarcl2  17985  prfval  18151  gsumval  18596  gsumval2  18605  frmdss2  18744  ghmrn  19105  cntzmhm2  19206  gsumval3  19775  gsumzaddlem  19789  dmdprdd  19869  dprdres  19898  dprdf1  19903  dprd2da  19912  dmdprdsplit2lem  19915  dmdprdsplit2  19916  dmdprdsplit  19917  dprdsplit  19918  dpjidcl  19928  ablfac1eulem  19942  ablfac1eu  19943  ablfaclem2  19956  ablfac2  19959  lmhmlsp  20660  frlmsslsp  21351  f1lindf  21377  mattpostpos  21956  iinopn  22404  lmbrf  22764  cnntri  22775  cnclsi  22776  lmcnp  22808  cnt0  22850  cnt1  22854  cnhaus  22858  cncmp  22896  connima  22929  1stcfb  22949  1stccnp  22966  1stckgenlem  23057  kgencn3  23062  txcnpi  23112  txcnp  23124  prdstps  23133  xkohaus  23157  xkoco2cn  23162  qtopeu  23220  hmeores  23275  fmfnfmlem2  23459  fmfnfmlem4  23461  fmfnfm  23462  lmflf  23509  txflf  23510  cnextfval  23566  cnextcn  23571  clssubg  23613  ghmcnp  23619  qustgplem  23625  tsmsval  23635  ucncn  23790  xmetdmdm  23841  metn0  23866  tmsval  23989  metustid  24063  metustexhalf  24065  metustfbas  24066  isngp2  24106  evth  24475  lmmbrf  24779  iscfil2  24783  caufval  24792  iscau2  24794  caucfil  24800  ovollb2  25006  ovolunlem1a  25013  ovoliunlem1  25019  ovoliun2  25023  ioombl1lem4  25078  uniioombllem1  25098  uniioombllem2  25100  uniioombllem6  25105  mbfconstlem  25144  ismbfcn  25146  mbfmulc2lem  25164  mbfmulc2re  25165  cncombf  25175  mbfaddlem  25177  mbflimsup  25183  i1f0rn  25199  itg1addlem5  25218  itg1climres  25232  mbfmullem2  25242  limcfval  25389  limcdif  25393  ellimc2  25394  ellimc3  25396  limccnp  25408  dvfval  25414  cpnord  25452  cpnres  25454  dvcmul  25461  dvcmulf  25462  dvexp  25470  dvgt0lem1  25519  dvcnvrelem1  25534  itgpowd  25567  plyaddlem1  25727  plymullem1  25728  plycpn  25802  aalioulem3  25847  tayl0  25874  dvntaylp  25883  ulm2  25897  ulmdvlem1  25912  xrlimcnp  26473  dchrelbas2  26740  dchrghm  26759  dchrptlem1  26767  dchrptlem2  26768  iscgrgd  27764  iscgrglt  27765  trgcgrg  27766  tgcgr4  27782  motcgrg  27795  wrdupgr  28345  wrdumgr  28357  grporndm  29763  sspn  29989  fmptcof2  31882  fnpreimac  31896  curry2ima  31930  fpwrelmap  31958  swrdf1  32120  pmtrcnel  32250  pmtrcnel2  32251  pmtrcnelor  32252  cycpmcl  32275  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem1  32285  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  cyc3co2  32299  cycpmconjv  32301  rmfsupp2  32387  rndrhmcl  32396  rhmpreimaidl  32537  elrspunidl  32546  rhmimaidl  32550  evls1dm  32641  ply1degltdimlem  32707  irngnzply1lem  32754  irngnzply1  32755  zarcmplem  32861  rhmpreimacnlem  32864  indf1ofs  33024  esumpcvgval  33076  ofcfval4  33103  measdivcst  33222  oms0  33296  omsmon  33297  omssubaddlem  33298  omssubadd  33299  carsgval  33302  omsmeas  33322  sitgclg  33341  eulerpartlemgu  33376  sseqfv2  33393  rrvdm  33445  ftc2re  33610  cvmliftmolem1  34272  cvmliftlem3  34278  cvmliftlem10  34285  cvmliftlem13  34287  cvmlift2lem9  34302  cvmlift3lem6  34315  cvmlift3lem7  34316  mclsax  34560  mclsppslem  34574  mclspps  34575  fwddifval  35134  fwddifnval  35135  bj-finsumval0  36166  curunc  36470  itg2addnclem2  36540  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem8  36568  sdclem2  36610  isbnd3  36652  ssbnd  36656  bnd2lem  36659  ismtyval  36668  grpokerinj  36761  rngosn3  36792  rngodm1dm2  36800  divrngcl  36825  isdrngo2  36826  sticksstones1  40962  evlselvlem  41158  mapfzcons2  41457  fnwe2lem2  41793  lmhmfgima  41826  wnefimgd  42913  binomcxplemnotnn0  43115  cncmpmax  43716  mullimcf  44339  limsuppnfdlem  44417  limsupvaluz  44424  climxrrelem  44465  climxrre  44466  liminfvalxr  44499  liminflimsupxrre  44533  xlimmnfvlem2  44549  xlimpnfvlem2  44553  xlimliminflimsup  44578  cncfuni  44602  cncficcgt0  44604  cncfioobd  44613  dvsinax  44629  itgperiod  44697  fvvolioof  44705  fvvolicof  44707  stoweidlem29  44745  fourierdlem20  44843  fourierdlem53  44875  fourierdlem63  44885  fourierdlem68  44890  fourierdlem82  44904  sge0sn  45095  sge0tsms  45096  sge0cl  45097  sge0isum  45143  ismeannd  45183  hoicvr  45264  dmovn  45320  hspmbl  45345  ovolval4lem1  45365  ovnovollem1  45372  ovnovollem2  45373  issmfd  45451  issmfdf  45453  cnfsmf  45456  issmfled  45473  issmfgtd  45477  smfsuplem1  45527  smfdivdmmbl2  45557  fcores  45777  f1cof1blem  45784  f1cof1b  45785  funfocofob  45786  rmsuppss  47046  mndpsuppss  47047  itcovalendof  47355