Theorem fdm 5410

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4660   Fn wfn 5250  ⟶wf 5251

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 5258  df-f 5259

This theorem is referenced by:  fdmd  5411  fdmi  5412  fssxp  5422  ffdm  5425  dmfex  5444  f00  5446  f0dom0  5448  f0rn0  5449  foima  5482  fimadmfo  5486  foco  5488  resdif  5523  fimacnv  5688  dff3im  5704  ffvresb  5722  resflem  5723  fmptco  5725  focdmex  6169  issmo2  6344  smoiso  6357  tfrcllemubacc  6414  rdgon  6441  frecabcl  6454  frecsuclem  6461  mapprc  6708  elpm2r  6722  map0b  6743  mapsn  6746  brdomg  6804  pw2f1odclem  6892  fopwdom  6894  casef  7149  nn0supp  9295  frecuzrdgdomlem  10491  frecuzrdgsuctlem  10497  zfz1isolemiso  10913  ennnfonelemex  12574  intopsn  12953  iscnp3  14382  cnpnei  14398  cnntr  14404  cncnp  14409  cndis  14420  psmetdmdm  14503  xmetres  14561  metres  14562  metcnp  14691  dvcj  14888  nninfall  15569