Theorem fndmd 6622

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

Syntax hints:   → wi 4   = wceq 1559  dom cdm 5645   Fn wfn 6512

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 209  df-an 400  df-fn 6520

This theorem is referenced by:  fdm  6697  f1dm  6762  f1odm  6806  f1o00  6838  fvelimad  6930  rescnvimafod  7050  f1eqcocnv  7281  ofrfvalg  7664  offval  7665  fndmexd  7881  dmmpoga  8050  fnwelem  8106  frrlem4  8265  frrlem8  8269  frrlem10  8271  fpr2  8280  fprresex  8286  wfr2  8303  tfrlem5  8345  ixpiunwdom  9535  frr2  9715  dfac12lem1  10097  ackbij2lem3  10193  itunisuc  10373  ttukeylem3  10465  prdsbas2  17481  prdsplusgval  17485  prdsmulrval  17487  prdsleval  17489  prdsvscaval  17491  imasleval  17554  ssclem  17835  isssc  17836  rescval2  17844  issubc2  17852  cofuval  17898  resfval2  17909  resf1st  17910  resf2nd  17911  prdsmgp  20180  lspextmo  21103  dsmmfi  21770  ofco2  22491  neiss2  23141  txdis1cn  23675  qtopcld  23753  qtoprest  23757  kqsat  23771  kqdisj  23772  isr0  23777  elfm3  23990  ovolunlem1  25539  ofpreima  32817  ofpreima2  32818  fnpreimac  32822  fsuppcurry1  32876  fsuppcurry2  32877  pfxf1  33081  s2rnOLD  33083  s3rnOLD  33085  cycpmfvlem  33253  cycpmfv1  33254  cycpmfv2  33255  cycpmfv3  33256  1arithidomlem2  33693  1arithidom  33694  esplyind  33833  ply1annidllem  33959  ofcfval  34356  probfinmeasb  34686  bnj564  35004  bnj1121  35244  bnj1442  35308  bnj1450  35309  bnj1501  35326  fnrelpredd  35351  onvfowev  35423  sdclem2  38205  prdstotbnd  38257  diadm  41623  dibdiadm  41743  dibdmN  41745  dicdmN  41772  dihdm  41857  aks4d1p1p5  42656  aks6d1c6lem2  42752  tfsconcat0b  43887  fnchoice  45573  wessf1ornlem  45727  limsupequzlem  46260  climrescn  46286  icccncfext  46425  stoweidlem35  46573  stoweidlem59  46597  smflimmpt  47348  smflimsuplem7  47364  iinfssclem1  49639  infsubc2d  49647  oppfvallem  49720  funcoppc3  49732  uptposlem  49782