Theorem fdm 5488

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4725   Fn wfn 5321  ⟶wf 5322

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 5329  df-f 5330

This theorem is referenced by:  fdmd  5489  fdmi  5490  fssxp  5502  ffdm  5505  dmfex  5526  f00  5528  f0dom0  5530  f0rn0  5531  foima  5564  fimadmfo  5568  foco  5570  resdif  5605  fimacnv  5776  dff3im  5792  ffvresb  5810  resflem  5811  fmptco  5813  focdmex  6277  issmo2  6455  smoiso  6468  tfrcllemubacc  6525  rdgon  6552  frecabcl  6565  frecsuclem  6572  mapprc  6821  elpm2r  6835  map0b  6856  mapsn  6859  brdomg  6919  pw2f1odclem  7020  fopwdom  7022  casef  7287  nn0supp  9454  frecuzrdgdomlem  10680  frecuzrdgsuctlem  10686  zfz1isolemiso  11104  ennnfonelemex  13040  intopsn  13455  iscnp3  14933  cnpnei  14949  cnntr  14955  cncnp  14960  cndis  14971  psmetdmdm  15054  xmetres  15112  metres  15113  metcnp  15242  dvcj  15439  wlkm  16196  upgr2wlkdc  16234  wlkres  16236  nninfall  16637