Theorem fdm 5441

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

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4683   Fn wfn 5275  ⟶wf 5276

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 5283  df-f 5284

This theorem is referenced by:  fdmd  5442  fdmi  5443  fssxp  5453  ffdm  5456  dmfex  5477  f00  5479  f0dom0  5481  f0rn0  5482  foima  5515  fimadmfo  5519  foco  5521  resdif  5556  fimacnv  5722  dff3im  5738  ffvresb  5756  resflem  5757  fmptco  5759  focdmex  6213  issmo2  6388  smoiso  6401  tfrcllemubacc  6458  rdgon  6485  frecabcl  6498  frecsuclem  6505  mapprc  6752  elpm2r  6766  map0b  6787  mapsn  6790  brdomg  6850  pw2f1odclem  6946  fopwdom  6948  casef  7205  nn0supp  9367  frecuzrdgdomlem  10584  frecuzrdgsuctlem  10590  zfz1isolemiso  11006  ennnfonelemex  12860  intopsn  13274  iscnp3  14750  cnpnei  14766  cnntr  14772  cncnp  14777  cndis  14788  psmetdmdm  14871  xmetres  14929  metres  14930  metcnp  15059  dvcj  15256  nninfall  16087