Theorem f1odm 5646

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4776   Fn wfn 5375  –1-1-onto→wf1o 5379

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  df-f1 5385  df-f1o 5387

This theorem is used by:  f1imacnv  5659  f1opw2  6299  en2  7118  xpcomco  7130  mapen  7152  ssenen  7158  phplem4  7162  phplem4on  7175  dif1en  7189  fiintim  7244  caseinl  7438  caseinr  7439  ctssdccl  7458  fihasheqf1oi  11248  hashfacen  11306  fisumss  12184  ballotfilemrv  13321