Theorem fdm 5430

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

Syntax hints:   → wi 4   = wceq 1372  dom cdm 4674   Fn wfn 5265  ⟶wf 5266

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 5273  df-f 5274

This theorem is referenced by:  fdmd  5431  fdmi  5432  fssxp  5442  ffdm  5445  dmfex  5464  f00  5466  f0dom0  5468  f0rn0  5469  foima  5502  fimadmfo  5506  foco  5508  resdif  5543  fimacnv  5708  dff3im  5724  ffvresb  5742  resflem  5743  fmptco  5745  focdmex  6199  issmo2  6374  smoiso  6387  tfrcllemubacc  6444  rdgon  6471  frecabcl  6484  frecsuclem  6491  mapprc  6738  elpm2r  6752  map0b  6773  mapsn  6776  brdomg  6836  pw2f1odclem  6930  fopwdom  6932  casef  7189  nn0supp  9346  frecuzrdgdomlem  10560  frecuzrdgsuctlem  10566  zfz1isolemiso  10982  ennnfonelemex  12727  intopsn  13141  iscnp3  14617  cnpnei  14633  cnntr  14639  cncnp  14644  cndis  14655  psmetdmdm  14738  xmetres  14796  metres  14797  metcnp  14926  dvcj  15123  nninfall  15879