Theorem fdm 5478

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4718   Fn wfn 5312  ⟶wf 5313

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 5320  df-f 5321

This theorem is referenced by:  fdmd  5479  fdmi  5480  fssxp  5490  ffdm  5493  dmfex  5514  f00  5516  f0dom0  5518  f0rn0  5519  foima  5552  fimadmfo  5556  foco  5558  resdif  5593  fimacnv  5763  dff3im  5779  ffvresb  5797  resflem  5798  fmptco  5800  focdmex  6258  issmo2  6433  smoiso  6446  tfrcllemubacc  6503  rdgon  6530  frecabcl  6543  frecsuclem  6550  mapprc  6797  elpm2r  6811  map0b  6832  mapsn  6835  brdomg  6895  pw2f1odclem  6991  fopwdom  6993  casef  7251  nn0supp  9417  frecuzrdgdomlem  10634  frecuzrdgsuctlem  10640  zfz1isolemiso  11056  ennnfonelemex  12980  intopsn  13395  iscnp3  14871  cnpnei  14887  cnntr  14893  cncnp  14898  cndis  14909  psmetdmdm  14992  xmetres  15050  metres  15051  metcnp  15180  dvcj  15377  wlkm  16038  nninfall  16334