Theorem fndmd 6598

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5625   Fn wfn 6488

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 6496

This theorem is referenced by:  fdm  6672  f1dm  6735  f1o00  6810  fvelimad  6902  rescnvimafod  7020  f1eqcocnv  7249  ofrfvalg  7632  offval  7633  fndmexd  7848  dmmpoga  8019  fnwelem  8075  frrlem4  8233  frrlem8  8237  frrlem10  8239  fpr2  8248  fprresex  8254  wfr2  8271  tfrlem5  8313  ixpiunwdom  9499  frr2  9676  dfac12lem1  10058  ackbij2lem3  10154  itunisuc  10333  ttukeylem3  10425  prdsbas2  17393  prdsplusgval  17397  prdsmulrval  17399  prdsleval  17401  prdsvscaval  17403  imasleval  17466  ssclem  17747  isssc  17748  rescval2  17756  issubc2  17764  cofuval  17810  resfval2  17821  resf1st  17822  resf2nd  17823  prdsmgp  20090  lspextmo  21012  dsmmfi  21697  ofco2  22399  neiss2  23049  txdis1cn  23583  qtopcld  23661  qtoprest  23665  kqsat  23679  kqdisj  23680  isr0  23685  elfm3  23898  ovolunlem1  25458  ofpreima  32725  ofpreima2  32726  fnpreimac  32730  fsuppcurry1  32784  fsuppcurry2  32785  pfxf1  33005  s2rnOLD  33007  s3rnOLD  33009  cycpmfvlem  33175  cycpmfv1  33176  cycpmfv2  33177  cycpmfv3  33178  1arithidomlem2  33598  1arithidom  33599  esplyind  33712  ply1annidllem  33839  ofcfval  34236  probfinmeasb  34566  bnj564  34881  bnj1121  35122  bnj1442  35186  bnj1450  35187  bnj1501  35204  fnrelpredd  35228  sdclem2  37920  prdstotbnd  37972  diadm  41338  dibdiadm  41458  dibdmN  41460  dicdmN  41487  dihdm  41572  aks4d1p1p5  42372  aks6d1c6lem2  42468  tfsconcat0b  43630  fnchoice  45316  wessf1ornlem  45471  limsupequzlem  46008  climrescn  46034  icccncfext  46173  stoweidlem35  46321  stoweidlem59  46345  smflimmpt  47096  smflimsuplem7  47112  iinfssclem1  49341  infsubc2d  49349  oppfvallem  49422  funcoppc3  49434  uptposlem  49484