Theorem fdmd 6698

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638  ⟶wf 6507

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 6514  df-f 6515

This theorem is referenced by:  fssdmd  6706  fssdm  6707  foima  6777  focnvimacdmdm  6784  resdif  6821  fssrescdmd  7098  fmptco  7101  funfvima2d  7206  focdmex  7934  suppsnop  8157  onnseq  8313  fopwdom  9049  fodomfib  9280  fodomfibOLD  9282  intrnfi  9367  ordtypelem5  9475  ordtypelem6  9476  ordtypelem7  9477  ordtypelem8  9478  brwdomn0  9522  wdomtr  9528  fseqenlem2  9978  fin23lem30  10295  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  fin1a2lem7  10359  ttukeylem6  10467  fodomb  10479  pwxpndom2  10618  hashf1lem1  14420  wrddm  14486  swrdcl  14610  cats1un  14686  repswswrd  14749  limsupgle  15443  limsupgre  15447  rlim  15461  rlimi  15479  lo1o1  15498  rlimuni  15516  o1co  15552  rlimcn1  15554  ruclem11  16208  1arith  16898  ramval  16979  0ram  16991  mrcuni  17582  homarcl2  17997  prfval  18160  gsumval  18604  gsumval2  18613  mndpsuppss  18692  frmdss2  18790  ghmrn  19161  cntzmhm2  19274  gsumval3  19837  gsumzaddlem  19851  dmdprdd  19931  dprdres  19960  dprdf1  19965  dprd2da  19974  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dmdprdsplit  19979  dprdsplit  19980  dpjidcl  19990  ablfac1eulem  20004  ablfac1eu  20005  ablfaclem2  20018  ablfac2  20021  lmhmlsp  20956  rhmpreimaidl  21187  frlmsslsp  21705  f1lindf  21731  mattpostpos  22341  iinopn  22789  lmbrf  23147  cnntri  23158  cnclsi  23159  lmcnp  23191  cnt0  23233  cnt1  23237  cnhaus  23241  cncmp  23279  connima  23312  1stcfb  23332  1stccnp  23349  1stckgenlem  23440  kgencn3  23445  txcnpi  23495  txcnp  23507  prdstps  23516  xkohaus  23540  xkoco2cn  23545  qtopeu  23603  hmeores  23658  fmfnfmlem2  23842  fmfnfmlem4  23844  fmfnfm  23845  lmflf  23892  txflf  23893  cnextfval  23949  cnextcn  23954  clssubg  23996  ghmcnp  24002  qustgplem  24008  tsmsval  24018  ucncn  24172  xmetdmdm  24223  metn0  24248  tmsval  24369  metustid  24442  metustexhalf  24444  metustfbas  24445  isngp2  24485  evth  24858  lmmbrf  25162  iscfil2  25166  caufval  25175  iscau2  25177  caucfil  25183  ovollb2  25390  ovolunlem1a  25397  ovoliunlem1  25403  ovoliun2  25407  ioombl1lem4  25462  uniioombllem1  25482  uniioombllem2  25484  uniioombllem6  25489  mbfconstlem  25528  ismbfcn  25530  mbfmulc2lem  25548  mbfmulc2re  25549  cncombf  25559  mbfaddlem  25561  mbflimsup  25567  i1f0rn  25583  itg1addlem5  25601  itg1climres  25615  mbfmullem2  25625  limcfval  25773  limcdif  25777  ellimc2  25778  ellimc3  25780  limccnp  25792  dvfval  25798  cpnord  25837  cpnres  25839  dvcmul  25847  dvcmulf  25848  dvexp  25857  dvgt0lem1  25907  dvcnvrelem1  25922  itgpowd  25957  plyaddlem1  26118  plymullem1  26119  plycpn  26197  aalioulem3  26242  tayl0  26269  dvntaylp  26279  ulm2  26294  ulmdvlem1  26309  xrlimcnp  26878  dchrelbas2  27148  dchrghm  27167  dchrptlem1  27175  dchrptlem2  27176  iscgrgd  28440  iscgrglt  28441  trgcgrg  28442  tgcgr4  28458  motcgrg  28471  wrdupgr  29012  wrdumgr  29024  grporndm  30439  sspn  30665  fmptcof2  32581  fnpreimac  32595  curry2ima  32632  fpwrelmap  32656  indf1ofs  32789  ccatdmss  32871  swrdf1  32878  pfxchn  32935  chnind  32937  chnccats1  32941  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  wrdpmtrlast  33050  cycpmcl  33073  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem1  33083  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cyc3co2  33097  cycpmconjv  33099  fxpgaval  33124  rmfsupp2  33189  elrgspnsubrunlem2  33199  rndrhmcl  33246  elrspunidl  33399  rhmimaidl  33403  1arithidomlem2  33507  1arithidom  33508  evls1dm  33530  ply1degltdimlem  33618  fldextrspunlsp  33669  irngnzply1lem  33685  irngnzply1  33686  zarcmplem  33871  rhmpreimacnlem  33874  esumpcvgval  34068  ofcfval4  34095  measdivcst  34214  oms0  34288  omsmon  34289  omssubaddlem  34290  omssubadd  34291  carsgval  34294  omsmeas  34314  sitgclg  34333  eulerpartlemgu  34368  sseqfv2  34385  rrvdm  34437  ftc2re  34589  cvmliftmolem1  35268  cvmliftlem3  35274  cvmliftlem10  35281  cvmliftlem13  35283  cvmlift2lem9  35298  cvmlift3lem6  35311  cvmlift3lem7  35312  mclsax  35556  mclsppslem  35570  mclspps  35571  fwddifval  36150  fwddifnval  36151  weiunfrlem  36452  bj-finsumval0  37273  curunc  37596  itg2addnclem2  37666  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem8  37694  sdclem2  37736  isbnd3  37778  ssbnd  37782  bnd2lem  37785  ismtyval  37794  grpokerinj  37887  rngosn3  37918  rngodm1dm2  37926  divrngcl  37951  isdrngo2  37952  sticksstones1  42134  aks5lem2  42175  evlselvlem  42574  mapfzcons2  42707  fnwe2lem2  43040  lmhmfgima  43073  wnefimgd  44150  binomcxplemnotnn0  44345  cncmpmax  45026  mullimcf  45621  limsuppnfdlem  45699  limsupvaluz  45706  climxrrelem  45747  climxrre  45748  liminfvalxr  45781  liminflimsupxrre  45815  xlimmnfvlem2  45831  xlimpnfvlem2  45835  xlimliminflimsup  45860  cncfuni  45884  cncficcgt0  45886  cncfioobd  45895  dvsinax  45911  itgperiod  45979  fvvolioof  45987  fvvolicof  45989  stoweidlem29  46027  fourierdlem20  46125  fourierdlem53  46157  fourierdlem63  46167  fourierdlem68  46172  fourierdlem82  46186  sge0sn  46377  sge0tsms  46378  sge0cl  46379  sge0isum  46425  ismeannd  46465  hoicvr  46546  dmovn  46602  hspmbl  46627  ovolval4lem1  46647  ovnovollem1  46654  ovnovollem2  46655  issmfd  46733  issmfdf  46735  cnfsmf  46738  issmfled  46755  issmfgtd  46759  smfsuplem1  46809  smfdivdmmbl2  46839  fcores  47068  f1cof1blem  47075  f1cof1b  47078  funfocofob  47079  rmsuppss  48358  itcovalendof  48658  ffvbr  48844  lmdran  49660  cmdlan  49661