Theorem fdm 5539

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5533	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 5480	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4774   Fn wfn 5372  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  fdmd  5540  fdmi  5541  fssxp  5555  ffdm  5558  dmfex  5582  f00  5584  f0dom0  5586  f0rn0  5587  foima  5620  fimadmfo  5624  foco  5626  resdif  5661  fimacnv  5837  dff3im  5853  ffvresb  5871  resflem  5872  fmptco  5874  focdmex  6344  fsuppeq  6487  fsuppeqg  6488  issmo2  6560  smoiso  6573  tfrcllemubacc  6630  rdgon  6657  frecabcl  6670  frecsuclem  6677  mapprc  6926  elpm2r  6940  map0b  6968  mapsnd  6970  mapsn  6972  brdomg  7032  pw2f1odclem  7134  fopwdom  7136  casef  7429  nn0supp  9624  frecuzrdgdomlem  10869  frecuzrdgsuctlem  10875  zfz1isolemiso  11307  ennnfonelemex  13357  intopsn  13740  iscnp3  15395  cnpnei  15411  cnntr  15417  cncnp  15422  cndis  15433  psmetdmdm  15516  xmetres  15574  metres  15575  metcnp  15704  dvcj  15901  wlkm  16746  upgr2wlkdc  16784  wlkres  16786  nninfall  17218