Theorem fndmd 6597

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 6595	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5624   Fn wfn 6487

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 6495

This theorem is referenced by:  fdm  6671  f1dm  6734  f1o00  6809  fvelimad  6901  rescnvimafod  7019  f1eqcocnv  7249  ofrfvalg  7632  offval  7633  fndmexd  7848  dmmpoga  8019  fnwelem  8074  frrlem4  8232  frrlem8  8236  frrlem10  8238  fpr2  8247  fprresex  8253  wfr2  8270  tfrlem5  8312  ixpiunwdom  9498  frr2  9675  dfac12lem1  10057  ackbij2lem3  10153  itunisuc  10332  ttukeylem3  10424  prdsbas2  17423  prdsplusgval  17427  prdsmulrval  17429  prdsleval  17431  prdsvscaval  17433  imasleval  17496  ssclem  17777  isssc  17778  rescval2  17786  issubc2  17794  cofuval  17840  resfval2  17851  resf1st  17852  resf2nd  17853  prdsmgp  20123  lspextmo  21043  dsmmfi  21728  ofco2  22426  neiss2  23076  txdis1cn  23610  qtopcld  23688  qtoprest  23692  kqsat  23706  kqdisj  23707  isr0  23712  elfm3  23925  ovolunlem1  25474  ofpreima  32753  ofpreima2  32754  fnpreimac  32758  fsuppcurry1  32812  fsuppcurry2  32813  pfxf1  33017  s2rnOLD  33019  s3rnOLD  33021  cycpmfvlem  33188  cycpmfv1  33189  cycpmfv2  33190  cycpmfv3  33191  1arithidomlem2  33611  1arithidom  33612  esplyind  33734  ply1annidllem  33861  ofcfval  34258  probfinmeasb  34588  bnj564  34903  bnj1121  35143  bnj1442  35207  bnj1450  35208  bnj1501  35225  fnrelpredd  35250  sdclem2  38077  prdstotbnd  38129  diadm  41495  dibdiadm  41615  dibdmN  41617  dicdmN  41644  dihdm  41729  aks4d1p1p5  42528  aks6d1c6lem2  42624  tfsconcat0b  43792  fnchoice  45478  wessf1ornlem  45633  limsupequzlem  46168  climrescn  46194  icccncfext  46333  stoweidlem35  46481  stoweidlem59  46505  smflimmpt  47256  smflimsuplem7  47272  iinfssclem1  49541  infsubc2d  49549  oppfvallem  49622  funcoppc3  49634  uptposlem  49684