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

Theorem f1dm 5645
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 5642 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 fndm 5546 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 16 1  |-  ( F : A -1-1-> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   dom cdm 4880    Fn wfn 5451   -1-1->wf1 5453
This theorem is referenced by:  fun11iun  5697  fnwelem  6463  tposf12  6506  fodomr  7260  domssex  7270  acndom  7934  acndom2  7937  ackbij1b  8121  fin1a2lem6  8287  cnt0  17412  cnt1  17416  cnhaus  17420  hmeoimaf1o  17804  uslgra1  21394  usgra1  21395  ctex  24102  rankeq1o  26114  hfninf  26129  eldioph2lem2  26821
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 179  df-an 362  df-fn 5459  df-f 5460  df-f1 5461
  Copyright terms: Public domain W3C validator