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

Theorem f1dm 5441
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 5438 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 fndm 5343 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 15 1  |-  ( F : A -1-1-> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   dom cdm 4689    Fn wfn 5250   -1-1->wf1 5252
This theorem is referenced by:  fun11iun  5493  fnwelem  6230  tposf12  6259  fodomr  7012  domssex  7022  acndom  7678  acndom2  7681  ackbij1b  7865  fin1a2lem6  8031  cnt0  17074  cnt1  17078  cnhaus  17082  hmeoimaf1o  17461  ctex  23336  rankeq1o  24801  hfninf  24816  eldioph2lem2  26840  uslgra1  28118  usgra1  28119
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258  df-f 5259  df-f1 5260
  Copyright terms: Public domain W3C validator