Theorem fdm 5479

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 5473	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 5420	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4719   Fn wfn 5313  ⟶wf 5314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-fn 5321  df-f 5322

This theorem is referenced by:  fdmd  5480  fdmi  5481  fssxp  5493  ffdm  5496  dmfex  5517  f00  5519  f0dom0  5521  f0rn0  5522  foima  5555  fimadmfo  5559  foco  5561  resdif  5596  fimacnv  5766  dff3im  5782  ffvresb  5800  resflem  5801  fmptco  5803  focdmex  6266  issmo2  6441  smoiso  6454  tfrcllemubacc  6511  rdgon  6538  frecabcl  6551  frecsuclem  6558  mapprc  6807  elpm2r  6821  map0b  6842  mapsn  6845  brdomg  6905  pw2f1odclem  7003  fopwdom  7005  casef  7266  nn0supp  9432  frecuzrdgdomlem  10651  frecuzrdgsuctlem  10657  zfz1isolemiso  11074  ennnfonelemex  13000  intopsn  13415  iscnp3  14892  cnpnei  14908  cnntr  14914  cncnp  14919  cndis  14930  psmetdmdm  15013  xmetres  15071  metres  15072  metcnp  15201  dvcj  15398  wlkm  16080  upgr2wlkdc  16116  wlkres  16118  nninfall  16435