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

Theorem f1dm 5708
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 5705 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 fndm 5608 . 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 1370   dom cdm 4938    Fn wfn 5511   -1-1->wf1 5513
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 5519  df-f 5520  df-f1 5521
This theorem is referenced by:  fun11iun  6637  fnwelem  6787  tposf12  6870  fodomr  7562  domssex  7572  acndom  8322  acndom2  8325  ackbij1b  8509  fin1a2lem6  8675  cnt0  19066  cnt1  19070  cnhaus  19074  hmeoimaf1o  19459  uslgra1  23426  usgra1  23427  ctex  26142  rankeq1o  28343  hfninf  28358  eldioph2lem2  29237
  Copyright terms: Public domain W3C validator