Theorem fdm 5343

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

Syntax hints:   → wi 4   = wceq 1343  dom cdm 4604   Fn wfn 5183  ⟶wf 5184

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

This theorem depends on definitions:  df-bi 116  df-fn 5191  df-f 5192

This theorem is referenced by:  fdmd  5344  fdmi  5345  fssxp  5355  ffdm  5358  dmfex  5377  f00  5379  f0dom0  5381  f0rn0  5382  foima  5415  foco  5420  resdif  5454  fimacnv  5614  dff3im  5630  ffvresb  5648  resflem  5649  fmptco  5651  fornex  6083  issmo2  6257  smoiso  6270  tfrcllemubacc  6327  rdgon  6354  frecabcl  6367  frecsuclem  6374  mapprc  6618  elpm2r  6632  map0b  6653  mapsn  6656  brdomg  6714  fopwdom  6802  casef  7053  nn0supp  9166  frecuzrdgdomlem  10352  frecuzrdgsuctlem  10358  zfz1isolemiso  10752  ennnfonelemex  12347  intopsn  12598  iscnp3  12853  cnpnei  12869  cnntr  12875  cncnp  12880  cndis  12891  psmetdmdm  12974  xmetres  13032  metres  13033  metcnp  13162  dvcj  13323  nninfall  13899