Theorem fndmd 6652

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5676   Fn wfn 6536

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 398  df-fn 6544

This theorem is referenced by:  fdm  6724  f1dm  6789  f1o00  6866  fvelimad  6957  rescnvimafod  7073  f1eqcocnv  7296  ofrfvalg  7675  offval  7676  fndmexd  7894  dmmpoga  8056  fnwelem  8114  frrlem4  8271  frrlem8  8275  frrlem10  8277  fpr2  8286  fprresex  8292  wfrlem17OLD  8322  wfr2  8333  tfrlem5  8377  ixpiunwdom  9582  frr2  9752  dfac12lem1  10135  ackbij2lem3  10233  itunisuc  10411  ttukeylem3  10503  prdsbas2  17412  prdsplusgval  17416  prdsmulrval  17418  prdsleval  17420  prdsvscaval  17422  imasleval  17484  ssclem  17763  isssc  17764  rescval2  17772  issubc2  17783  cofuval  17829  resfval2  17840  resf1st  17841  resf2nd  17842  prdsmgp  20126  lspextmo  20660  dsmmfi  21285  ofco2  21945  neiss2  22597  txdis1cn  23131  qtopcld  23209  qtoprest  23213  kqsat  23227  kqdisj  23228  isr0  23233  elfm3  23446  ovolunlem1  25006  ofpreima  31878  ofpreima2  31879  fnpreimac  31884  fsuppcurry1  31938  fsuppcurry2  31939  pfxf1  32096  s2rn  32098  s3rn  32100  cycpmfvlem  32259  cycpmfv1  32260  cycpmfv2  32261  cycpmfv3  32262  ply1annidllem  32751  ofcfval  33085  probfinmeasb  33416  bnj564  33744  bnj1121  33985  bnj1442  34049  bnj1450  34050  bnj1501  34067  fnrelpredd  34081  sdclem2  36599  prdstotbnd  36651  diadm  39895  dibdiadm  40015  dibdmN  40017  dicdmN  40044  dihdm  40129  aks4d1p1p5  40929  tfsconcat0b  42082  fnchoice  43699  wessf1ornlem  43868  limsupequzlem  44425  climrescn  44451  icccncfext  44590  stoweidlem35  44738  stoweidlem59  44762  smflimmpt  45513  smflimsuplem7  45529