Theorem fdm 5416

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

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

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

This theorem is referenced by:  fdmd  5417  fdmi  5418  fssxp  5428  ffdm  5431  dmfex  5450  f00  5452  f0dom0  5454  f0rn0  5455  foima  5488  fimadmfo  5492  foco  5494  resdif  5529  fimacnv  5694  dff3im  5710  ffvresb  5728  resflem  5729  fmptco  5731  focdmex  6181  issmo2  6356  smoiso  6369  tfrcllemubacc  6426  rdgon  6453  frecabcl  6466  frecsuclem  6473  mapprc  6720  elpm2r  6734  map0b  6755  mapsn  6758  brdomg  6816  pw2f1odclem  6904  fopwdom  6906  casef  7163  nn0supp  9320  frecuzrdgdomlem  10528  frecuzrdgsuctlem  10534  zfz1isolemiso  10950  ennnfonelemex  12658  intopsn  13071  iscnp3  14547  cnpnei  14563  cnntr  14569  cncnp  14574  cndis  14585  psmetdmdm  14668  xmetres  14726  metres  14727  metcnp  14856  dvcj  15053  nninfall  15764