Theorem fdmd 6746

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685  ⟶wf 6557

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 6564  df-f 6565

This theorem is referenced by:  fssdmd  6754  fssdm  6755  foima  6825  focnvimacdmdm  6832  resdif  6869  fssrescdmd  7146  fmptco  7149  funfvima2d  7252  focdmex  7980  suppsnop  8203  onnseq  8384  fopwdom  9120  fodomfib  9369  fodomfibOLD  9371  intrnfi  9456  ordtypelem5  9562  ordtypelem6  9563  ordtypelem7  9564  ordtypelem8  9565  brwdomn0  9609  wdomtr  9615  fseqenlem2  10065  fin23lem30  10382  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  fin1a2lem7  10446  ttukeylem6  10554  fodomb  10566  pwxpndom2  10705  hashf1lem1  14494  wrddm  14559  swrdcl  14683  cats1un  14759  repswswrd  14822  limsupgle  15513  limsupgre  15517  rlim  15531  rlimi  15549  lo1o1  15568  rlimuni  15586  o1co  15622  rlimcn1  15624  ruclem11  16276  1arith  16965  ramval  17046  0ram  17058  mrcuni  17664  homarcl2  18080  prfval  18244  gsumval  18690  gsumval2  18699  mndpsuppss  18778  frmdss2  18876  ghmrn  19247  cntzmhm2  19360  gsumval3  19925  gsumzaddlem  19939  dmdprdd  20019  dprdres  20048  dprdf1  20053  dprd2da  20062  dmdprdsplit2lem  20065  dmdprdsplit2  20066  dmdprdsplit  20067  dprdsplit  20068  dpjidcl  20078  ablfac1eulem  20092  ablfac1eu  20093  ablfaclem2  20106  ablfac2  20109  lmhmlsp  21048  rhmpreimaidl  21287  frlmsslsp  21816  f1lindf  21842  mattpostpos  22460  iinopn  22908  lmbrf  23268  cnntri  23279  cnclsi  23280  lmcnp  23312  cnt0  23354  cnt1  23358  cnhaus  23362  cncmp  23400  connima  23433  1stcfb  23453  1stccnp  23470  1stckgenlem  23561  kgencn3  23566  txcnpi  23616  txcnp  23628  prdstps  23637  xkohaus  23661  xkoco2cn  23666  qtopeu  23724  hmeores  23779  fmfnfmlem2  23963  fmfnfmlem4  23965  fmfnfm  23966  lmflf  24013  txflf  24014  cnextfval  24070  cnextcn  24075  clssubg  24117  ghmcnp  24123  qustgplem  24129  tsmsval  24139  ucncn  24294  xmetdmdm  24345  metn0  24370  tmsval  24493  metustid  24567  metustexhalf  24569  metustfbas  24570  isngp2  24610  evth  24991  lmmbrf  25296  iscfil2  25300  caufval  25309  iscau2  25311  caucfil  25317  ovollb2  25524  ovolunlem1a  25531  ovoliunlem1  25537  ovoliun2  25541  ioombl1lem4  25596  uniioombllem1  25616  uniioombllem2  25618  uniioombllem6  25623  mbfconstlem  25662  ismbfcn  25664  mbfmulc2lem  25682  mbfmulc2re  25683  cncombf  25693  mbfaddlem  25695  mbflimsup  25701  i1f0rn  25717  itg1addlem5  25735  itg1climres  25749  mbfmullem2  25759  limcfval  25907  limcdif  25911  ellimc2  25912  ellimc3  25914  limccnp  25926  dvfval  25932  cpnord  25971  cpnres  25973  dvcmul  25981  dvcmulf  25982  dvexp  25991  dvgt0lem1  26041  dvcnvrelem1  26056  itgpowd  26091  plyaddlem1  26252  plymullem1  26253  plycpn  26331  aalioulem3  26376  tayl0  26403  dvntaylp  26413  ulm2  26428  ulmdvlem1  26443  xrlimcnp  27011  dchrelbas2  27281  dchrghm  27300  dchrptlem1  27308  dchrptlem2  27309  iscgrgd  28521  iscgrglt  28522  trgcgrg  28523  tgcgr4  28539  motcgrg  28552  wrdupgr  29102  wrdumgr  29114  grporndm  30529  sspn  30755  fmptcof2  32667  fnpreimac  32681  curry2ima  32718  fpwrelmap  32744  indf1ofs  32851  ccatdmss  32934  swrdf1  32941  pfxchn  32999  chnind  33001  chnccats1  33005  pmtrcnel  33109  pmtrcnel2  33110  pmtrcnelor  33111  wrdpmtrlast  33113  cycpmcl  33136  cycpmco2f1  33144  cycpmco2rn  33145  cycpmco2lem1  33146  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  cyc3co2  33160  cycpmconjv  33162  rmfsupp2  33242  elrgspnsubrunlem2  33252  rndrhmcl  33299  elrspunidl  33456  rhmimaidl  33460  1arithidomlem2  33564  1arithidom  33565  evls1dm  33587  ply1degltdimlem  33673  fldextrspunlsp  33724  irngnzply1lem  33740  irngnzply1  33741  zarcmplem  33880  rhmpreimacnlem  33883  esumpcvgval  34079  ofcfval4  34106  measdivcst  34225  oms0  34299  omsmon  34300  omssubaddlem  34301  omssubadd  34302  carsgval  34305  omsmeas  34325  sitgclg  34344  eulerpartlemgu  34379  sseqfv2  34396  rrvdm  34448  ftc2re  34613  cvmliftmolem1  35286  cvmliftlem3  35292  cvmliftlem10  35299  cvmliftlem13  35301  cvmlift2lem9  35316  cvmlift3lem6  35329  cvmlift3lem7  35330  mclsax  35574  mclsppslem  35588  mclspps  35589  fwddifval  36163  fwddifnval  36164  weiunfrlem  36465  bj-finsumval0  37286  curunc  37609  itg2addnclem2  37679  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem8  37707  sdclem2  37749  isbnd3  37791  ssbnd  37795  bnd2lem  37798  ismtyval  37807  grpokerinj  37900  rngosn3  37931  rngodm1dm2  37939  divrngcl  37964  isdrngo2  37965  sticksstones1  42147  aks5lem2  42188  evlselvlem  42596  mapfzcons2  42730  fnwe2lem2  43063  lmhmfgima  43096  wnefimgd  44174  binomcxplemnotnn0  44375  cncmpmax  45037  mullimcf  45638  limsuppnfdlem  45716  limsupvaluz  45723  climxrrelem  45764  climxrre  45765  liminfvalxr  45798  liminflimsupxrre  45832  xlimmnfvlem2  45848  xlimpnfvlem2  45852  xlimliminflimsup  45877  cncfuni  45901  cncficcgt0  45903  cncfioobd  45912  dvsinax  45928  itgperiod  45996  fvvolioof  46004  fvvolicof  46006  stoweidlem29  46044  fourierdlem20  46142  fourierdlem53  46174  fourierdlem63  46184  fourierdlem68  46189  fourierdlem82  46203  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0isum  46442  ismeannd  46482  hoicvr  46563  dmovn  46619  hspmbl  46644  ovolval4lem1  46664  ovnovollem1  46671  ovnovollem2  46672  issmfd  46750  issmfdf  46752  cnfsmf  46755  issmfled  46772  issmfgtd  46776  smfsuplem1  46826  smfdivdmmbl2  46856  fcores  47079  f1cof1blem  47086  f1cof1b  47089  funfocofob  47090  rmsuppss  48286  itcovalendof  48590