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

Theorem f1dm 5778
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 5775 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 fndm 5673 . 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 1374   dom cdm 4994    Fn wfn 5576   -1-1->wf1 5578
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 371  df-fn 5584  df-f 5585  df-f1 5586
This theorem is referenced by:  fun11iun  6736  fnwelem  6890  tposf12  6972  fodomr  7660  domssex  7670  acndom  8423  acndom2  8426  ackbij1b  8610  fin1a2lem6  8776  cnt0  19608  cnt1  19612  cnhaus  19616  hmeoimaf1o  20001  uslgra1  24036  usgra1  24037  ctex  27191  rankeq1o  29393  hfninf  29408  eldioph2lem2  30287  f1dmvrnfibi  31738  f1vrnfibi  31739
  Copyright terms: Public domain W3C validator