Theorem fdmd 6757

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700  ⟶wf 6569

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 6576  df-f 6577

This theorem is referenced by:  fssdmd  6765  fssdm  6766  foima  6839  focnvimacdmdm  6846  resdif  6883  fssrescdmd  7160  fmptco  7163  funfvima2d  7269  focdmex  7996  suppsnop  8219  onnseq  8400  fopwdom  9146  fodomfib  9397  fodomfibOLD  9399  intrnfi  9485  ordtypelem5  9591  ordtypelem6  9592  ordtypelem7  9593  ordtypelem8  9594  brwdomn0  9638  wdomtr  9644  fseqenlem2  10094  fin23lem30  10411  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  fin1a2lem7  10475  ttukeylem6  10583  fodomb  10595  pwxpndom2  10734  hashf1lem1  14504  wrddm  14569  swrdcl  14693  cats1un  14769  repswswrd  14832  limsupgle  15523  limsupgre  15527  rlim  15541  rlimi  15559  lo1o1  15578  rlimuni  15596  o1co  15632  rlimcn1  15634  ruclem11  16288  1arith  16974  ramval  17055  0ram  17067  mrcuni  17679  homarcl2  18102  prfval  18268  gsumval  18715  gsumval2  18724  frmdss2  18898  ghmrn  19269  cntzmhm2  19382  gsumval3  19949  gsumzaddlem  19963  dmdprdd  20043  dprdres  20072  dprdf1  20077  dprd2da  20086  dmdprdsplit2lem  20089  dmdprdsplit2  20090  dmdprdsplit  20091  dprdsplit  20092  dpjidcl  20102  ablfac1eulem  20116  ablfac1eu  20117  ablfaclem2  20130  ablfac2  20133  lmhmlsp  21071  rhmpreimaidl  21310  frlmsslsp  21839  f1lindf  21865  mattpostpos  22481  iinopn  22929  lmbrf  23289  cnntri  23300  cnclsi  23301  lmcnp  23333  cnt0  23375  cnt1  23379  cnhaus  23383  cncmp  23421  connima  23454  1stcfb  23474  1stccnp  23491  1stckgenlem  23582  kgencn3  23587  txcnpi  23637  txcnp  23649  prdstps  23658  xkohaus  23682  xkoco2cn  23687  qtopeu  23745  hmeores  23800  fmfnfmlem2  23984  fmfnfmlem4  23986  fmfnfm  23987  lmflf  24034  txflf  24035  cnextfval  24091  cnextcn  24096  clssubg  24138  ghmcnp  24144  qustgplem  24150  tsmsval  24160  ucncn  24315  xmetdmdm  24366  metn0  24391  tmsval  24514  metustid  24588  metustexhalf  24590  metustfbas  24591  isngp2  24631  evth  25010  lmmbrf  25315  iscfil2  25319  caufval  25328  iscau2  25330  caucfil  25336  ovollb2  25543  ovolunlem1a  25550  ovoliunlem1  25556  ovoliun2  25560  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem2  25637  uniioombllem6  25642  mbfconstlem  25681  ismbfcn  25683  mbfmulc2lem  25701  mbfmulc2re  25702  cncombf  25712  mbfaddlem  25714  mbflimsup  25720  i1f0rn  25736  itg1addlem5  25755  itg1climres  25769  mbfmullem2  25779  limcfval  25927  limcdif  25931  ellimc2  25932  ellimc3  25934  limccnp  25946  dvfval  25952  cpnord  25991  cpnres  25993  dvcmul  26001  dvcmulf  26002  dvexp  26011  dvgt0lem1  26061  dvcnvrelem1  26076  itgpowd  26111  plyaddlem1  26272  plymullem1  26273  plycpn  26349  aalioulem3  26394  tayl0  26421  dvntaylp  26431  ulm2  26446  ulmdvlem1  26461  xrlimcnp  27029  dchrelbas2  27299  dchrghm  27318  dchrptlem1  27326  dchrptlem2  27327  iscgrgd  28539  iscgrglt  28540  trgcgrg  28541  tgcgr4  28557  motcgrg  28570  wrdupgr  29120  wrdumgr  29132  grporndm  30542  sspn  30768  fmptcof2  32675  fnpreimac  32689  curry2ima  32720  fpwrelmap  32747  ccatdmss  32916  swrdf1  32923  pfxchn  32982  chnind  32983  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  wrdpmtrlast  33086  cycpmcl  33109  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem1  33119  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cyc3co2  33133  cycpmconjv  33135  rmfsupp2  33218  rndrhmcl  33265  elrspunidl  33421  rhmimaidl  33425  1arithidomlem2  33529  1arithidom  33530  evls1dm  33552  ply1degltdimlem  33635  irngnzply1lem  33690  irngnzply1  33691  zarcmplem  33827  rhmpreimacnlem  33830  indf1ofs  33990  esumpcvgval  34042  ofcfval4  34069  measdivcst  34188  oms0  34262  omsmon  34263  omssubaddlem  34264  omssubadd  34265  carsgval  34268  omsmeas  34288  sitgclg  34307  eulerpartlemgu  34342  sseqfv2  34359  rrvdm  34411  ftc2re  34575  cvmliftmolem1  35249  cvmliftlem3  35255  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem9  35279  cvmlift3lem6  35292  cvmlift3lem7  35293  mclsax  35537  mclsppslem  35551  mclspps  35552  fwddifval  36126  fwddifnval  36127  weiunfrlem  36430  bj-finsumval0  37251  curunc  37562  itg2addnclem2  37632  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem8  37660  sdclem2  37702  isbnd3  37744  ssbnd  37748  bnd2lem  37751  ismtyval  37760  grpokerinj  37853  rngosn3  37884  rngodm1dm2  37892  divrngcl  37917  isdrngo2  37918  sticksstones1  42103  aks5lem2  42144  evlselvlem  42541  mapfzcons2  42675  fnwe2lem2  43008  lmhmfgima  43041  wnefimgd  44123  binomcxplemnotnn0  44325  cncmpmax  44932  mullimcf  45544  limsuppnfdlem  45622  limsupvaluz  45629  climxrrelem  45670  climxrre  45671  liminfvalxr  45704  liminflimsupxrre  45738  xlimmnfvlem2  45754  xlimpnfvlem2  45758  xlimliminflimsup  45783  cncfuni  45807  cncficcgt0  45809  cncfioobd  45818  dvsinax  45834  itgperiod  45902  fvvolioof  45910  fvvolicof  45912  stoweidlem29  45950  fourierdlem20  46048  fourierdlem53  46080  fourierdlem63  46090  fourierdlem68  46095  fourierdlem82  46109  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0isum  46348  ismeannd  46388  hoicvr  46469  dmovn  46525  hspmbl  46550  ovolval4lem1  46570  ovnovollem1  46577  ovnovollem2  46578  issmfd  46656  issmfdf  46658  cnfsmf  46661  issmfled  46678  issmfgtd  46682  smfsuplem1  46732  smfdivdmmbl2  46762  fcores  46982  f1cof1blem  46989  f1cof1b  46992  funfocofob  46993  rmsuppss  48095  mndpsuppss  48096  itcovalendof  48403