Theorem f1dm 6105

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1dm	|- ( F : A -1-1-> B -> dom F = A )

Proof of Theorem f1dm

Step	Hyp	Ref	Expression
1		f1fn 6102	. 2 |- ( F : A -1-1-> B -> F Fn A )
2		fndm 5990	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 17	1 |- ( F : A -1-1-> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1483   dom cdm 5114   Fn wfn 5883   -1-1->wf1 5885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-fn 5891  df-f 5892  df-f1 5893

This theorem is referenced by:  fun11iun  7126  fnwelem  7292  tposf12  7377  ctex  7970  fodomr  8111  domssex  8121  f1dmvrnfibi  8250  f1vrnfibi  8251  acndom  8874  acndom2  8877  ackbij1b  9061  fin1a2lem6  9227  cnt0  21150  cnt1  21154  cnhaus  21158  hmeoimaf1o  21573  uspgr1e  26136  rankeq1o  32278  hfninf  32293  eldioph2lem2  37324