Theorem fndmd 6605

Description: The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fndmd.1	⊢ (𝜑 → 𝐹 Fn 𝐴)

Assertion

Ref	Expression
fndmd	⊢ (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fndmd

Step	Hyp	Ref	Expression
1		fndmd.1	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		fndm 6603	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5632   Fn wfn 6495

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 6503

This theorem is referenced by:  fdm  6679  f1dm  6742  f1o00  6817  fvelimad  6909  rescnvimafod  7027  f1eqcocnv  7257  ofrfvalg  7640  offval  7641  fndmexd  7856  dmmpoga  8027  fnwelem  8083  frrlem4  8241  frrlem8  8245  frrlem10  8247  fpr2  8256  fprresex  8262  wfr2  8279  tfrlem5  8321  ixpiunwdom  9507  frr2  9684  dfac12lem1  10066  ackbij2lem3  10162  itunisuc  10341  ttukeylem3  10433  prdsbas2  17401  prdsplusgval  17405  prdsmulrval  17407  prdsleval  17409  prdsvscaval  17411  imasleval  17474  ssclem  17755  isssc  17756  rescval2  17764  issubc2  17772  cofuval  17818  resfval2  17829  resf1st  17830  resf2nd  17831  prdsmgp  20098  lspextmo  21020  dsmmfi  21705  ofco2  22407  neiss2  23057  txdis1cn  23591  qtopcld  23669  qtoprest  23673  kqsat  23687  kqdisj  23688  isr0  23693  elfm3  23906  ovolunlem1  25466  ofpreima  32754  ofpreima2  32755  fnpreimac  32759  fsuppcurry1  32813  fsuppcurry2  32814  pfxf1  33034  s2rnOLD  33036  s3rnOLD  33038  cycpmfvlem  33205  cycpmfv1  33206  cycpmfv2  33207  cycpmfv3  33208  1arithidomlem2  33628  1arithidom  33629  esplyind  33751  ply1annidllem  33878  ofcfval  34275  probfinmeasb  34605  bnj564  34920  bnj1121  35160  bnj1442  35224  bnj1450  35225  bnj1501  35242  fnrelpredd  35266  sdclem2  37987  prdstotbnd  38039  diadm  41405  dibdiadm  41525  dibdmN  41527  dicdmN  41554  dihdm  41639  aks4d1p1p5  42439  aks6d1c6lem2  42535  tfsconcat0b  43697  fnchoice  45383  wessf1ornlem  45538  limsupequzlem  46074  climrescn  46100  icccncfext  46239  stoweidlem35  46387  stoweidlem59  46411  smflimmpt  47162  smflimsuplem7  47178  iinfssclem1  49407  infsubc2d  49415  oppfvallem  49488  funcoppc3  49500  uptposlem  49550