Theorem f1odm 5623

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4754   Fn wfn 5352  –1-1-onto→wf1o 5356

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 5360  df-f 5361  df-f1 5362  df-f1o 5364

This theorem is referenced by:  f1imacnv  5636  f1opw2  6269  en2  7078  xpcomco  7090  mapen  7112  ssenen  7118  phplem4  7122  phplem4on  7135  dif1en  7149  fiintim  7204  caseinl  7395  caseinr  7396  ctssdccl  7415  fihasheqf1oi  11175  hashfacen  11233  fisumss  12103  ballotfilemrv  13207