Theorem f1odm 5618

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 5615	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5455	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4749   Fn wfn 5347   -1-1-onto->wf1o 5351

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 5355  df-f 5356  df-f1 5357  df-f1o 5359

This theorem is referenced by:  f1imacnv  5631  f1opw2  6261  en2  7065  xpcomco  7077  mapen  7099  ssenen  7105  phplem4  7109  phplem4on  7122  dif1en  7136  fiintim  7191  caseinl  7382  caseinr  7383  ctssdccl  7402  fihasheqf1oi  11150  hashfacen  11208  fisumss  12078