Theorem f1odm 5646

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

Assertion

Ref	Expression
f1odm	|- ( F : A -1-1-onto-> B -> dom F = A )

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 5643	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5483	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> dom F = A )

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  7437  caseinr  7438  ctssdccl  7457  fihasheqf1oi  11247  hashfacen  11305  fisumss  12183  ballotfilemrv  13320