Theorem fdmd 6742

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  ⟶wf 6554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6561  df-f 6562

This theorem is used by:  fssdmd  6750  fssdm  6751  foima  6823  focnvimacdmdm  6830  resdif  6868  fssrescdmd  7151  fmptco  7154  funfvima2d  7261  focdmex  7992  suppsnop  8223  onnseq  8380  fopwdom  9132  fodomfib  9348  intrnfi  9435  ordtypelem5  9543  ordtypelem6  9544  ordtypelem7  9545  ordtypelem8  9546  brwdomn0  9590  wdomtr  9596  fseqenlem2  10131  fin23lem30  10447  isf34lem5  10483  isf34lem7  10484  isf34lem6  10485  fin1a2lem7  10511  ttukeylem6  10619  fodomb  10632  pwxpndom2  10777  hashf1lem1  14627  wrddm  14693  ccatdmss  14754  swrdcl  14821  swrdf1  14827  cats1un  14898  repswswrd  14963  limsupgle  15673  limsupgre  15677  rlim  15691  rlimi  15709  lo1o1  15728  rlimuni  15746  o1co  15782  rlimcn1  15784  ruclem11  16437  1arith  17134  ramval  17215  0ram  17227  mrcuni  17824  homarcl2  18239  prfval  18402  pfxchn  18813  chnind  18824  chnccats1  18828  chnccat  18829  gsumval  18895  gsumval2  18904  mndpsuppss  18988  frmdss2  19088  ghmrn  19472  cntzmhm2  19586  gsumval3  20151  gsumzaddlem  20165  dmdprdd  20245  dprdres  20274  dprdf1  20279  dprd2da  20288  dmdprdsplit2lem  20291  dmdprdsplit2  20292  dmdprdsplit  20293  dprdsplit  20294  dpjidcl  20304  ablfac1eulem  20318  ablfac1eu  20319  ablfaclem2  20332  ablfac2  20335  crngrhmfo  20756  lmhmlsp  21354  rhmpreimaidl  21601  frlmsslsp  22132  f1lindf  22158  mattpostpos  22799  iinopn  23250  lmbrf  23608  cnntri  23619  cnclsi  23620  lmcnp  23652  cnt0  23694  cnt1  23698  cnhaus  23702  cncmp  23740  connima  23773  1stcfb  23793  1stccnp  23811  1stckgenlem  23902  kgencn3  23907  txcnpi  23957  txcnp  23969  prdstps  23978  xkohaus  24002  xkoco2cn  24007  qtopeu  24065  hmeores  24120  fmfnfmlem2  24304  fmfnfmlem4  24306  fmfnfm  24307  lmflf  24354  txflf  24355  cnextfval  24411  cnextcn  24416  clssubg  24458  ghmcnp  24464  qustgplem  24470  tsmsval  24480  ucncn  24633  xmetdmdm  24684  metn0  24709  tmsval  24830  metustid  24903  metustexhalf  24905  metustfbas  24906  isngp2  24946  evth  25310  lmmbrf  25613  iscfil2  25617  caufval  25626  iscau2  25628  caucfil  25634  ovollb2  25840  ovolunlem1a  25847  ovoliunlem1  25853  ovoliun2  25857  ioombl1lem4  25912  uniioombllem1  25932  uniioombllem2  25934  uniioombllem6  25939  mbfconstlem  25978  ismbfcn  25980  mbfmulc2lem  25998  mbfmulc2re  25999  cncombf  26009  mbfaddlem  26011  mbflimsup  26017  i1f0rn  26033  itg1addlem5  26051  itg1climres  26065  mbfmullem2  26075  limcfval  26222  limcdif  26226  ellimc2  26227  ellimc3  26229  limccnp  26241  dvfval  26247  cpnord  26285  cpnres  26287  dvcmul  26294  dvcmulf  26295  dvexp  26303  dvgt0lem1  26352  dvcnvrelem1  26367  itgpowd  26400  plyaddlem1  26562  plymullem1  26563  plycpn  26640  rnplynfin  26660  plyconz  26661  aalioulem3  26691  tayl0  26719  dvntaylp  26728  ulm2  26742  ulmdvlem1  26757  xrlimcnp  27326  dchrelbas2  27594  dchrghm  27613  dchrptlem1  27621  dchrptlem2  27622  iscgrgd  29006  iscgrglt  29007  trgcgrg  29008  tgcgr4  29024  motcgrg  29037  wrdupgr  29693  wrdumgr  29705  grporndm  31142  sspn  31368  fmptcof2  33323  fnpreimac  33336  curry2ima  33373  fpwrelmap  33395  indf1ofs  33503  pmtrcnel  33720  pmtrcnel2  33721  pmtrcnelor  33722  wrdpmtrlast  33724  cycpmcl  33747  cycpmco2f1  33755  cycpmco2rn  33756  cycpmco2lem1  33757  cycpmco2lem2  33758  cycpmco2lem3  33759  cycpmco2lem4  33760  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2lem7  33763  cycpmco2  33764  cyc3co2  33771  cycpmconjv  33773  fxpgaval  33798  rmfsupp2  33868  elrgspnsubrunlem2  33879  rndrhmcl  33928  elrspunidl  34048  rhmimaidl  34052  1arithidomlem2  34138  1arithidom  34139  evls1dm  34163  selvascl  34219  evlextv  34244  esplymhp  34270  esplysply  34273  esplyfval1  34275  ply1degltdimlem  34324  fldextrspunlsp  34376  irngnzply1lem  34392  irngnzply1  34393  zarcmplem  34583  rhmpreimacnlem  34586  esumpcvgval  34780  ofcfval4  34807  measdivcst  34927  oms0  34999  omsmon  35000  omssubaddlem  35001  omssubadd  35002  carsgval  35005  omsmeas  35025  sitgclg  35044  eulerpartlemgu  35079  sseqfv2  35096  rrvdm  35148  ftc2re  35297  cvmliftmolem1  36213  cvmliftlem3  36219  cvmliftlem10  36226  cvmliftlem13  36228  cvmlift2lem9  36243  cvmlift3lem6  36256  cvmlift3lem7  36257  mclsax  36501  mclsppslem  36515  mclspps  36516  fwddifval  37105  fwddifnval  37106  weiunfrlem  37430  bj-finsumval0  38398  curunc  38717  itg2addnclem2  38782  ftc1anclem5  38807  ftc1anclem6  38808  ftc1anclem8  38810  sdclem2  38868  isbnd3  38910  ssbnd  38914  bnd2lem  38917  ismtyval  38926  grpokerinj  39019  rngosn3  39050  rngodm1dm2  39058  divrngcl  39083  isdrngo2  39084  sticksstones1  43388  aks5lem2  43429  evlselvlem  43809  mapfzcons2  43923  lmhmfgima  44279  wnefimgd  45353  binomcxplemnotnn0  45532  cncmpmax  46254  mullimcf  46840  limsuppnfdlem  46916  limsupvaluz  46923  climxrrelem  46964  climxrre  46965  liminfvalxr  46998  liminflimsupxrre  47032  xlimmnfvlem2  47048  xlimpnfvlem2  47052  xlimliminflimsup  47077  cncfuni  47101  cncficcgt0  47103  cncfioobd  47112  dvsinax  47128  itgperiod  47196  fvvolioof  47204  fvvolicof  47206  stoweidlem29  47244  fourierdlem20  47342  fourierdlem48  47369  fourierdlem49  47370  fourierdlem53  47374  fourierdlem63  47384  fourierdlem68  47389  fourierdlem82  47403  fourierdlem113  47434  sge0sn  47594  sge0tsms  47595  sge0cl  47596  sge0isum  47642  ismeannd  47682  hoicvr  47763  dmovn  47819  hspmbl  47844  ovolval4lem1  47864  ovnovollem1  47871  ovnovollem2  47872  issmfd  47950  issmfdf  47952  cnfsmf  47955  issmfled  47972  issmfgtd  47976  smfsuplem1  48026  smfdivdmmbl2  48056  tmachlem-agreesn  48162  fcores  48342  f1cof1blem  48349  f1cof1b  48352  funfocofob  48353  rmsuppss  49687  itcovalendof  49986  ffvbr  50172  termccofix  50876  lmdran  51059  cmdlan  51060