Theorem f1odm 5575

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 5572	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5419	. 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 1395   dom cdm 4718   Fn wfn 5312   -1-1-onto->wf1o 5316

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 5320  df-f 5321  df-f1 5322  df-f1o 5324

This theorem is referenced by:  f1imacnv  5588  f1opw2  6210  en2  6971  xpcomco  6981  mapen  7003  ssenen  7008  phplem4  7012  phplem4on  7025  dif1en  7037  fiintim  7089  caseinl  7254  caseinr  7255  ctssdccl  7274  fihasheqf1oi  11004  hashfacen  11053  fisumss  11898