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  9318  frecuzrdgdomlem  10526  frecuzrdgsuctlem  10532  zfz1isolemiso  10948  ennnfonelemex  12656  intopsn  13069  iscnp3  14523  cnpnei  14539  cnntr  14545  cncnp  14550  cndis  14561  psmetdmdm  14644  xmetres  14702  metres  14703  metcnp  14832  dvcj  15029  nninfall  15740