Theorem fdm 5539

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4774   Fn wfn 5372  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  fdmd  5540  fdmi  5541  fssxp  5555  ffdm  5558  dmfex  5582  f00  5584  f0dom0  5586  f0rn0  5587  foima  5620  fimadmfo  5624  foco  5626  resdif  5661  fimacnv  5837  dff3im  5853  ffvresb  5871  resflem  5872  fmptco  5874  focdmex  6344  fsuppeq  6487  fsuppeqg  6488  issmo2  6560  smoiso  6573  tfrcllemubacc  6630  rdgon  6657  frecabcl  6670  frecsuclem  6677  mapprc  6926  elpm2r  6940  map0b  6968  mapsnd  6970  mapsn  6972  brdomg  7032  pw2f1odclem  7134  fopwdom  7136  casef  7428  nn0supp  9623  frecuzrdgdomlem  10867  frecuzrdgsuctlem  10873  zfz1isolemiso  11305  ennnfonelemex  13354  intopsn  13736  iscnp3  15353  cnpnei  15369  cnntr  15375  cncnp  15380  cndis  15391  psmetdmdm  15474  xmetres  15532  metres  15533  metcnp  15662  dvcj  15859  wlkm  16678  upgr2wlkdc  16716  wlkres  16718  nninfall  17150