Theorem fdmd 6719

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5667  ⟶wf 6530

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 396  df-fn 6537  df-f 6538

This theorem is referenced by:  fssdmd  6727  fssdm  6728  foima  6801  focnvimacdmdm  6808  resdif  6845  fmptco  7120  funfvima2d  7226  focdmex  7936  suppsnop  8158  onnseq  8340  fopwdom  9077  fodomfib  9323  intrnfi  9408  ordtypelem5  9514  ordtypelem6  9515  ordtypelem7  9516  ordtypelem8  9517  brwdomn0  9561  wdomtr  9567  fseqenlem2  10017  fin23lem30  10334  isf34lem5  10370  isf34lem7  10371  isf34lem6  10372  fin1a2lem7  10398  ttukeylem6  10506  fodomb  10518  pwxpndom2  10657  hashf1lem1  14413  hashf1lem1OLD  14414  wrddm  14469  swrdcl  14593  cats1un  14669  repswswrd  14732  limsupgle  15419  limsupgre  15423  rlim  15437  rlimi  15455  lo1o1  15474  rlimuni  15492  o1co  15528  rlimcn1  15530  ruclem11  16182  1arith  16861  ramval  16942  0ram  16954  mrcuni  17566  homarcl2  17989  prfval  18155  gsumval  18602  gsumval2  18611  frmdss2  18780  ghmrn  19146  cntzmhm2  19250  gsumval3  19819  gsumzaddlem  19833  dmdprdd  19913  dprdres  19942  dprdf1  19947  dprd2da  19956  dmdprdsplit2lem  19959  dmdprdsplit2  19960  dmdprdsplit  19961  dprdsplit  19962  dpjidcl  19972  ablfac1eulem  19986  ablfac1eu  19987  ablfaclem2  20000  ablfac2  20003  lmhmlsp  20889  frlmsslsp  21661  f1lindf  21687  mattpostpos  22280  iinopn  22728  lmbrf  23088  cnntri  23099  cnclsi  23100  lmcnp  23132  cnt0  23174  cnt1  23178  cnhaus  23182  cncmp  23220  connima  23253  1stcfb  23273  1stccnp  23290  1stckgenlem  23381  kgencn3  23386  txcnpi  23436  txcnp  23448  prdstps  23457  xkohaus  23481  xkoco2cn  23486  qtopeu  23544  hmeores  23599  fmfnfmlem2  23783  fmfnfmlem4  23785  fmfnfm  23786  lmflf  23833  txflf  23834  cnextfval  23890  cnextcn  23895  clssubg  23937  ghmcnp  23943  qustgplem  23949  tsmsval  23959  ucncn  24114  xmetdmdm  24165  metn0  24190  tmsval  24313  metustid  24387  metustexhalf  24389  metustfbas  24390  isngp2  24430  evth  24809  lmmbrf  25114  iscfil2  25118  caufval  25127  iscau2  25129  caucfil  25135  ovollb2  25342  ovolunlem1a  25349  ovoliunlem1  25355  ovoliun2  25359  ioombl1lem4  25414  uniioombllem1  25434  uniioombllem2  25436  uniioombllem6  25441  mbfconstlem  25480  ismbfcn  25482  mbfmulc2lem  25500  mbfmulc2re  25501  cncombf  25511  mbfaddlem  25513  mbflimsup  25519  i1f0rn  25535  itg1addlem5  25554  itg1climres  25568  mbfmullem2  25578  limcfval  25725  limcdif  25729  ellimc2  25730  ellimc3  25732  limccnp  25744  dvfval  25750  cpnord  25789  cpnres  25791  dvcmul  25799  dvcmulf  25800  dvexp  25809  dvgt0lem1  25859  dvcnvrelem1  25874  itgpowd  25909  plyaddlem1  26069  plymullem1  26070  plycpn  26145  aalioulem3  26190  tayl0  26217  dvntaylp  26226  ulm2  26240  ulmdvlem1  26255  xrlimcnp  26819  dchrelbas2  27089  dchrghm  27108  dchrptlem1  27116  dchrptlem2  27117  iscgrgd  28236  iscgrglt  28237  trgcgrg  28238  tgcgr4  28254  motcgrg  28267  wrdupgr  28817  wrdumgr  28829  grporndm  30235  sspn  30461  fmptcof2  32354  fnpreimac  32368  curry2ima  32402  fpwrelmap  32430  swrdf1  32590  pmtrcnel  32721  pmtrcnel2  32722  pmtrcnelor  32723  cycpmcl  32746  cycpmco2f1  32754  cycpmco2rn  32755  cycpmco2lem1  32756  cycpmco2lem2  32757  cycpmco2lem3  32758  cycpmco2lem4  32759  cycpmco2lem5  32760  cycpmco2lem6  32761  cycpmco2lem7  32762  cycpmco2  32763  cyc3co2  32770  cycpmconjv  32772  rmfsupp2  32856  rndrhmcl  32865  rhmpreimaidl  33009  elrspunidl  33018  rhmimaidl  33022  evls1dm  33111  ply1degltdimlem  33189  irngnzply1lem  33237  irngnzply1  33238  zarcmplem  33353  rhmpreimacnlem  33356  indf1ofs  33516  esumpcvgval  33568  ofcfval4  33595  measdivcst  33714  oms0  33788  omsmon  33789  omssubaddlem  33790  omssubadd  33791  carsgval  33794  omsmeas  33814  sitgclg  33833  eulerpartlemgu  33868  sseqfv2  33885  rrvdm  33937  ftc2re  34101  cvmliftmolem1  34763  cvmliftlem3  34769  cvmliftlem10  34776  cvmliftlem13  34778  cvmlift2lem9  34793  cvmlift3lem6  34806  cvmlift3lem7  34807  mclsax  35051  mclsppslem  35065  mclspps  35066  fwddifval  35630  fwddifnval  35631  bj-finsumval0  36657  curunc  36964  itg2addnclem2  37034  ftc1anclem5  37059  ftc1anclem6  37060  ftc1anclem8  37062  sdclem2  37104  isbnd3  37146  ssbnd  37150  bnd2lem  37153  ismtyval  37162  grpokerinj  37255  rngosn3  37286  rngodm1dm2  37294  divrngcl  37319  isdrngo2  37320  sticksstones1  41459  evlselvlem  41651  mapfzcons2  41971  fnwe2lem2  42307  lmhmfgima  42340  wnefimgd  43427  binomcxplemnotnn0  43629  cncmpmax  44230  mullimcf  44849  limsuppnfdlem  44927  limsupvaluz  44934  climxrrelem  44975  climxrre  44976  liminfvalxr  45009  liminflimsupxrre  45043  xlimmnfvlem2  45059  xlimpnfvlem2  45063  xlimliminflimsup  45088  cncfuni  45112  cncficcgt0  45114  cncfioobd  45123  dvsinax  45139  itgperiod  45207  fvvolioof  45215  fvvolicof  45217  stoweidlem29  45255  fourierdlem20  45353  fourierdlem53  45385  fourierdlem63  45395  fourierdlem68  45400  fourierdlem82  45414  sge0sn  45605  sge0tsms  45606  sge0cl  45607  sge0isum  45653  ismeannd  45693  hoicvr  45774  dmovn  45830  hspmbl  45855  ovolval4lem1  45875  ovnovollem1  45882  ovnovollem2  45883  issmfd  45961  issmfdf  45963  cnfsmf  45966  issmfled  45983  issmfgtd  45987  smfsuplem1  46037  smfdivdmmbl2  46067  fcores  46287  f1cof1blem  46294  f1cof1b  46295  funfocofob  46296  rmsuppss  47260  mndpsuppss  47261  itcovalendof  47568