Theorem fdm 5425

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

Syntax hints:   → wi 4   = wceq 1372  dom cdm 4673   Fn wfn 5263  ⟶wf 5264

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 5271  df-f 5272

This theorem is referenced by:  fdmd  5426  fdmi  5427  fssxp  5437  ffdm  5440  dmfex  5459  f00  5461  f0dom0  5463  f0rn0  5464  foima  5497  fimadmfo  5501  foco  5503  resdif  5538  fimacnv  5703  dff3im  5719  ffvresb  5737  resflem  5738  fmptco  5740  focdmex  6190  issmo2  6365  smoiso  6378  tfrcllemubacc  6435  rdgon  6462  frecabcl  6475  frecsuclem  6482  mapprc  6729  elpm2r  6743  map0b  6764  mapsn  6767  brdomg  6825  pw2f1odclem  6913  fopwdom  6915  casef  7172  nn0supp  9329  frecuzrdgdomlem  10543  frecuzrdgsuctlem  10549  zfz1isolemiso  10965  ennnfonelemex  12704  intopsn  13117  iscnp3  14593  cnpnei  14609  cnntr  14615  cncnp  14620  cndis  14631  psmetdmdm  14714  xmetres  14772  metres  14773  metcnp  14902  dvcj  15099  nninfall  15810