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  7117  xpcomco  7129  mapen  7151  ssenen  7157  phplem4  7161  phplem4on  7174  dif1en  7188  fiintim  7243  caseinl  7438  caseinr  7439  ctssdccl  7458  fihasheqf1oi  11249  hashfacen  11307  fisumss  12185  ballotfilemrv  13322