Theorem fdm 5413

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4663   Fn wfn 5253  ⟶wf 5254

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 5261  df-f 5262

This theorem is referenced by:  fdmd  5414  fdmi  5415  fssxp  5425  ffdm  5428  dmfex  5447  f00  5449  f0dom0  5451  f0rn0  5452  foima  5485  fimadmfo  5489  foco  5491  resdif  5526  fimacnv  5691  dff3im  5707  ffvresb  5725  resflem  5726  fmptco  5728  focdmex  6172  issmo2  6347  smoiso  6360  tfrcllemubacc  6417  rdgon  6444  frecabcl  6457  frecsuclem  6464  mapprc  6711  elpm2r  6725  map0b  6746  mapsn  6749  brdomg  6807  pw2f1odclem  6895  fopwdom  6897  casef  7154  nn0supp  9301  frecuzrdgdomlem  10509  frecuzrdgsuctlem  10515  zfz1isolemiso  10931  ennnfonelemex  12631  intopsn  13010  iscnp3  14439  cnpnei  14455  cnntr  14461  cncnp  14466  cndis  14477  psmetdmdm  14560  xmetres  14618  metres  14619  metcnp  14748  dvcj  14945  nninfall  15653