Theorem fdm 5371

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4626   Fn wfn 5211  ⟶wf 5212

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 5219  df-f 5220

This theorem is referenced by:  fdmd  5372  fdmi  5373  fssxp  5383  ffdm  5386  dmfex  5405  f00  5407  f0dom0  5409  f0rn0  5410  foima  5443  foco  5448  resdif  5483  fimacnv  5645  dff3im  5661  ffvresb  5679  resflem  5680  fmptco  5682  focdmex  6115  issmo2  6289  smoiso  6302  tfrcllemubacc  6359  rdgon  6386  frecabcl  6399  frecsuclem  6406  mapprc  6651  elpm2r  6665  map0b  6686  mapsn  6689  brdomg  6747  fopwdom  6835  casef  7086  nn0supp  9226  frecuzrdgdomlem  10414  frecuzrdgsuctlem  10420  zfz1isolemiso  10814  ennnfonelemex  12409  intopsn  12780  iscnp3  13634  cnpnei  13650  cnntr  13656  cncnp  13661  cndis  13672  psmetdmdm  13755  xmetres  13813  metres  13814  metcnp  13943  dvcj  14104  nninfall  14678