Theorem f1odm 5535

Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1odm	⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 5532	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 5379	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4680   Fn wfn 5272  –1-1-onto→wf1o 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 5280  df-f 5281  df-f1 5282  df-f1o 5284

This theorem is referenced by:  f1imacnv  5548  f1opw2  6162  en2  6923  xpcomco  6933  mapen  6955  ssenen  6960  phplem4  6964  phplem4on  6976  dif1en  6988  fiintim  7040  caseinl  7205  caseinr  7206  ctssdccl  7225  fihasheqf1oi  10945  hashfacen  10994  fisumss  11753