Theorem fdmd 6702

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

Syntax hints:   → wi 4   = wceq 1561  dom cdm 5648  ⟶wf 6517

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 209  df-an 400  df-fn 6524  df-f 6525

This theorem is referenced by:  fssdmd  6710  fssdm  6711  foima  6783  focnvimacdmdm  6790  resdif  6828  fssrescdmd  7108  fmptco  7111  funfvima2d  7216  focdmex  7937  suppsnop  8158  onnseq  8315  fopwdom  9057  fodomfib  9272  intrnfi  9360  ordtypelem5  9468  ordtypelem6  9469  ordtypelem7  9470  ordtypelem8  9471  brwdomn0  9515  wdomtr  9521  fseqenlem2  9993  fin23lem30  10310  isf34lem5  10346  isf34lem7  10347  isf34lem6  10348  fin1a2lem7  10374  ttukeylem6  10482  fodomb  10494  pwxpndom2  10634  hashf1lem1  14478  wrddm  14544  ccatdmss  14605  swrdcl  14669  cats1un  14744  repswswrd  14807  limsupgle  15514  limsupgre  15518  rlim  15532  rlimi  15550  lo1o1  15569  rlimuni  15587  o1co  15623  rlimcn1  15625  ruclem11  16282  1arith  16973  ramval  17054  0ram  17066  mrcuni  17663  homarcl2  18078  prfval  18241  pfxchn  18652  chnind  18663  chnccats1  18667  chnccat  18668  gsumval  18721  gsumval2  18730  mndpsuppss  18809  frmdss2  18907  ghmrn  19279  cntzmhm2  19392  gsumval3  19957  gsumzaddlem  19971  dmdprdd  20051  dprdres  20080  dprdf1  20085  dprd2da  20094  dmdprdsplit2lem  20097  dmdprdsplit2  20098  dmdprdsplit  20099  dprdsplit  20100  dpjidcl  20110  ablfac1eulem  20124  ablfac1eu  20125  ablfaclem2  20138  ablfac2  20141  lmhmlsp  21123  rhmpreimaidl  21354  frlmsslsp  21855  f1lindf  21881  mattpostpos  22521  iinopn  22969  lmbrf  23327  cnntri  23338  cnclsi  23339  lmcnp  23371  cnt0  23413  cnt1  23417  cnhaus  23421  cncmp  23459  connima  23492  1stcfb  23512  1stccnp  23529  1stckgenlem  23620  kgencn3  23625  txcnpi  23675  txcnp  23687  prdstps  23696  xkohaus  23720  xkoco2cn  23725  qtopeu  23783  hmeores  23838  fmfnfmlem2  24022  fmfnfmlem4  24024  fmfnfm  24025  lmflf  24072  txflf  24073  cnextfval  24129  cnextcn  24134  clssubg  24176  ghmcnp  24182  qustgplem  24188  tsmsval  24198  ucncn  24351  xmetdmdm  24402  metn0  24427  tmsval  24548  metustid  24621  metustexhalf  24623  metustfbas  24624  isngp2  24664  evth  25028  lmmbrf  25331  iscfil2  25335  caufval  25344  iscau2  25346  caucfil  25352  ovollb2  25558  ovolunlem1a  25565  ovoliunlem1  25571  ovoliun2  25575  ioombl1lem4  25630  uniioombllem1  25650  uniioombllem2  25652  uniioombllem6  25657  mbfconstlem  25696  ismbfcn  25698  mbfmulc2lem  25716  mbfmulc2re  25717  cncombf  25727  mbfaddlem  25729  mbflimsup  25735  i1f0rn  25751  itg1addlem5  25769  itg1climres  25783  mbfmullem2  25793  limcfval  25941  limcdif  25945  ellimc2  25946  ellimc3  25948  limccnp  25960  dvfval  25966  cpnord  26004  cpnres  26006  dvcmul  26013  dvcmulf  26014  dvexp  26022  dvgt0lem1  26071  dvcnvrelem1  26086  itgpowd  26119  plyaddlem1  26280  plymullem1  26281  plycpn  26360  aalioulem3  26405  tayl0  26432  dvntaylp  26441  ulm2  26455  ulmdvlem1  26470  xrlimcnp  27040  dchrelbas2  27308  dchrghm  27327  dchrptlem1  27335  dchrptlem2  27336  iscgrgd  28689  iscgrglt  28690  trgcgrg  28691  tgcgr4  28707  motcgrg  28720  wrdupgr  29293  wrdumgr  29305  grporndm  30720  sspn  30946  fmptcof2  32865  fnpreimac  32878  curry2ima  32917  fpwrelmap  32941  indf1ofs  33050  swrdf1  33140  pmtrcnel  33275  pmtrcnel2  33276  pmtrcnelor  33277  wrdpmtrlast  33279  cycpmcl  33302  cycpmco2f1  33310  cycpmco2rn  33311  cycpmco2lem1  33312  cycpmco2lem2  33313  cycpmco2lem3  33314  cycpmco2lem4  33315  cycpmco2lem5  33316  cycpmco2lem6  33317  cycpmco2lem7  33318  cycpmco2  33319  cyc3co2  33326  cycpmconjv  33328  fxpgaval  33353  rmfsupp2  33424  elrgspnsubrunlem2  33435  rndrhmcl  33486  elrspunidl  33617  rhmimaidl  33621  1arithidomlem2  33735  1arithidom  33736  evls1dm  33760  selvascl  33816  evlextv  33841  esplymhp  33867  esplysply  33870  esplyfval1  33872  ply1degltdimlem  33921  fldextrspunlsp  33973  irngnzply1lem  33989  irngnzply1  33990  zarcmplem  34180  rhmpreimacnlem  34183  esumpcvgval  34377  ofcfval4  34404  measdivcst  34523  oms0  34596  omsmon  34597  omssubaddlem  34598  omssubadd  34599  carsgval  34602  omsmeas  34622  sitgclg  34641  eulerpartlemgu  34676  sseqfv2  34693  rrvdm  34745  ftc2re  34894  cvmliftmolem1  35636  cvmliftlem3  35642  cvmliftlem10  35649  cvmliftlem13  35651  cvmlift2lem9  35666  cvmlift3lem6  35679  cvmlift3lem7  35680  mclsax  35924  mclsppslem  35938  mclspps  35939  fwddifval  36517  fwddifnval  36518  weiunfrlem  36829  bj-finsumval0  37782  curunc  38106  itg2addnclem2  38176  ftc1anclem5  38201  ftc1anclem6  38202  ftc1anclem8  38204  sdclem2  38246  isbnd3  38288  ssbnd  38292  bnd2lem  38295  ismtyval  38304  grpokerinj  38397  rngosn3  38428  rngodm1dm2  38436  divrngcl  38461  isdrngo2  38462  sticksstones1  42768  aks5lem2  42809  evlselvlem  43175  mapfzcons2  43305  fnwe2lem2  43633  lmhmfgima  43666  wnefimgd  44742  binomcxplemnotnn0  44923  cncmpmax  45603  mullimcf  46190  limsuppnfdlem  46266  limsupvaluz  46273  climxrrelem  46314  climxrre  46315  liminfvalxr  46348  liminflimsupxrre  46382  xlimmnfvlem2  46398  xlimpnfvlem2  46402  xlimliminflimsup  46427  cncfuni  46451  cncficcgt0  46453  cncfioobd  46462  dvsinax  46478  itgperiod  46546  fvvolioof  46554  fvvolicof  46556  stoweidlem29  46594  fourierdlem20  46692  fourierdlem48  46719  fourierdlem49  46720  fourierdlem53  46724  fourierdlem63  46734  fourierdlem68  46739  fourierdlem82  46753  fourierdlem113  46784  sge0sn  46944  sge0tsms  46945  sge0cl  46946  sge0isum  46992  ismeannd  47032  hoicvr  47113  dmovn  47169  hspmbl  47194  ovolval4lem1  47214  ovnovollem1  47221  ovnovollem2  47222  issmfd  47300  issmfdf  47302  cnfsmf  47305  issmfled  47322  issmfgtd  47326  smfsuplem1  47376  smfdivdmmbl2  47406  fcores  47652  f1cof1blem  47659  f1cof1b  47662  funfocofob  47663  rmsuppss  48983  itcovalendof  49282  ffvbr  49468  lmdran  50283  cmdlan  50284