Theorem f1odm 5548

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 5545	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5392	. 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 1373   dom cdm 4693   Fn wfn 5285   -1-1-onto->wf1o 5289

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 5293  df-f 5294  df-f1 5295  df-f1o 5297

This theorem is referenced by:  f1imacnv  5561  f1opw2  6175  en2  6936  xpcomco  6946  mapen  6968  ssenen  6973  phplem4  6977  phplem4on  6990  dif1en  7002  fiintim  7054  caseinl  7219  caseinr  7220  ctssdccl  7239  fihasheqf1oi  10969  hashfacen  11018  fisumss  11818