Theorem f1odm 5643

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 5640	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5480	. 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 4774   Fn wfn 5372   -1-1-onto->wf1o 5376

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 5380  df-f 5381  df-f1 5382  df-f1o 5384

This theorem is used by:  f1imacnv  5656  f1opw2  6296  en2  7112  xpcomco  7124  mapen  7146  ssenen  7152  phplem4  7156  phplem4on  7169  dif1en  7183  fiintim  7238  caseinl  7431  caseinr  7432  ctssdccl  7451  fihasheqf1oi  11226  hashfacen  11284  fisumss  12159  ballotfilemrv  13263