Theorem f1odm 5638

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 5635	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fndm 5475	. 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 1402   dom cdm 4769   Fn wfn 5367   -1-1-onto->wf1o 5371

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 5375  df-f 5376  df-f1 5377  df-f1o 5379

This theorem is referenced by:  f1imacnv  5651  f1opw2  6286  en2  7102  xpcomco  7114  mapen  7136  ssenen  7142  phplem4  7146  phplem4on  7159  dif1en  7173  fiintim  7228  caseinl  7421  caseinr  7422  ctssdccl  7441  fihasheqf1oi  11204  hashfacen  11262  fisumss  12137  ballotfilemrv  13241