Theorem fndmd 6626

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641   Fn wfn 6509

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 6517

This theorem is referenced by:  fdm  6700  f1dm  6763  f1o00  6838  fvelimad  6931  rescnvimafod  7048  f1eqcocnv  7279  ofrfvalg  7664  offval  7665  fndmexd  7883  dmmpoga  8055  fnwelem  8113  frrlem4  8271  frrlem8  8275  frrlem10  8277  fpr2  8286  fprresex  8292  wfr2  8309  tfrlem5  8351  ixpiunwdom  9550  frr2  9720  dfac12lem1  10104  ackbij2lem3  10200  itunisuc  10379  ttukeylem3  10471  prdsbas2  17439  prdsplusgval  17443  prdsmulrval  17445  prdsleval  17447  prdsvscaval  17449  imasleval  17511  ssclem  17788  isssc  17789  rescval2  17797  issubc2  17805  cofuval  17851  resfval2  17862  resf1st  17863  resf2nd  17864  prdsmgp  20067  lspextmo  20970  dsmmfi  21654  ofco2  22345  neiss2  22995  txdis1cn  23529  qtopcld  23607  qtoprest  23611  kqsat  23625  kqdisj  23626  isr0  23631  elfm3  23844  ovolunlem1  25405  ofpreima  32596  ofpreima2  32597  fnpreimac  32602  fsuppcurry1  32655  fsuppcurry2  32656  pfxf1  32870  s2rnOLD  32872  s3rnOLD  32874  cycpmfvlem  33076  cycpmfv1  33077  cycpmfv2  33078  cycpmfv3  33079  1arithidomlem2  33514  1arithidom  33515  ply1annidllem  33698  ofcfval  34095  probfinmeasb  34426  bnj564  34741  bnj1121  34982  bnj1442  35046  bnj1450  35047  bnj1501  35064  fnrelpredd  35086  sdclem2  37743  prdstotbnd  37795  diadm  41036  dibdiadm  41156  dibdmN  41158  dicdmN  41185  dihdm  41270  aks4d1p1p5  42070  aks6d1c6lem2  42166  tfsconcat0b  43342  fnchoice  45030  wessf1ornlem  45186  limsupequzlem  45727  climrescn  45753  icccncfext  45892  stoweidlem35  46040  stoweidlem59  46064  smflimmpt  46815  smflimsuplem7  46831  iinfssclem1  49047  infsubc2d  49055  oppfvallem  49128  funcoppc3  49140  uptposlem  49190