MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1dm Structured version   Unicode version

Theorem f1dm 5693
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
StepHypRef Expression
1 f1fn 5690 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 fndm 5588 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 16 1  |-  ( F : A -1-1-> B  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   dom cdm 4913    Fn wfn 5491   -1-1->wf1 5493
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 185  df-an 369  df-fn 5499  df-f 5500  df-f1 5501
This theorem is referenced by:  fun11iun  6659  fnwelem  6814  tposf12  6898  fodomr  7587  domssex  7597  acndom  8345  acndom2  8348  ackbij1b  8532  fin1a2lem6  8698  cnt0  19933  cnt1  19937  cnhaus  19941  hmeoimaf1o  20356  uslgra1  24493  usgra1  24494  ctex  27680  rankeq1o  29981  hfninf  29996  eldioph2lem2  30859  f1dmvrnfibi  32633  f1vrnfibi  32634
  Copyright terms: Public domain W3C validator