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  7116  xpcomco  7128  mapen  7150  ssenen  7156  phplem4  7160  phplem4on  7173  dif1en  7187  fiintim  7242  caseinl  7437  caseinr  7438  ctssdccl  7457  fihasheqf1oi  11248  hashfacen  11306  fisumss  12184  ballotfilemrv  13321