Theorem fdm 5542

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4776   Fn wfn 5375  ⟶wf 5376

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 5383  df-f 5384

This theorem is used by:  fdmd  5543  fdmi  5544  fssxp  5558  ffdm  5561  dmfex  5585  f00  5587  f0dom0  5589  f0rn0  5590  foima  5623  fimadmfo  5627  foco  5629  resdif  5664  fimacnv  5840  dff3im  5856  ffvresb  5874  resflem  5875  fmptco  5877  focdmex  6348  fsuppeq  6491  fsuppeqg  6492  issmo2  6564  smoiso  6577  tfrcllemubacc  6634  rdgon  6661  frecabcl  6674  frecsuclem  6681  mapprc  6930  elpm2r  6944  map0b  6972  mapsnd  6974  mapsn  6976  brdomg  7036  pw2f1odclem  7138  fopwdom  7140  casef  7434  nn0supp  9630  frecuzrdgdomlem  10875  frecuzrdgsuctlem  10881  zfz1isolemiso  11313  ennnfonelemex  13363  intopsn  13746  iscnp3  15429  cnpnei  15445  cnntr  15451  cncnp  15456  cndis  15467  psmetdmdm  15550  xmetres  15608  metres  15609  metcnp  15738  dvcj  15935  wlkm  16785  upgr2wlkdc  16823  wlkres  16825  nninfall  17258