Theorem f1odm 5617

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4748   Fn wfn 5346  –1-1-onto→wf1o 5350

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 5354  df-f 5355  df-f1 5356  df-f1o 5358

This theorem is referenced by:  f1imacnv  5630  f1opw2  6260  en2  7064  xpcomco  7076  mapen  7098  ssenen  7104  phplem4  7108  phplem4on  7121  dif1en  7135  fiintim  7190  caseinl  7381  caseinr  7382  ctssdccl  7401  fihasheqf1oi  11148  hashfacen  11204  fisumss  12074