Theorem fndmd 6522

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580   Fn wfn 6413

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 206  df-an 396  df-fn 6421

This theorem is referenced by:  fdm  6593  f1dm  6658  f1o00  6734  fvelimad  6818  rescnvimafod  6933  f1eqcocnv  7153  ofrfvalg  7519  offval  7520  fndmexd  7727  dmmpoga  7886  fnwelem  7943  frrlem4  8076  frrlem8  8080  frrlem10  8082  fpr2  8091  fprresex  8097  wfrlem17OLD  8127  wfr2  8138  tfrlem5  8182  ixpiunwdom  9279  frr2  9449  dfac12lem1  9830  ackbij2lem3  9928  itunisuc  10106  ttukeylem3  10198  prdsbas2  17097  prdsplusgval  17101  prdsmulrval  17103  prdsleval  17105  prdsvscaval  17107  imasleval  17169  ssclem  17448  isssc  17449  rescval2  17457  issubc2  17467  cofuval  17513  resfval2  17524  resf1st  17525  resf2nd  17526  prdsmgp  19764  lspextmo  20233  dsmmfi  20855  ofco2  21508  neiss2  22160  txdis1cn  22694  qtopcld  22772  qtoprest  22776  kqsat  22790  kqdisj  22791  isr0  22796  elfm3  23009  ovolunlem1  24566  ofpreima  30904  ofpreima2  30905  fnpreimac  30910  fsuppcurry1  30962  fsuppcurry2  30963  pfxf1  31118  s2rn  31120  s3rn  31122  cycpmfvlem  31281  cycpmfv1  31282  cycpmfv2  31283  cycpmfv3  31284  ofcfval  31966  probfinmeasb  32295  bnj564  32624  bnj1121  32865  bnj1442  32929  bnj1450  32930  bnj1501  32947  fnrelpredd  32961  sdclem2  35827  prdstotbnd  35879  diadm  38976  dibdiadm  39096  dibdmN  39098  dicdmN  39125  dihdm  39210  aks4d1p1p5  40011  fnchoice  42461  wessf1ornlem  42611  limsupequzlem  43153  climrescn  43179  icccncfext  43318  stoweidlem35  43466  stoweidlem59  43490  smflimmpt  44230  smflimsuplem7  44246