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

Theorem f1dm 5457
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 5454 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 fndm 5359 . 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 1632   dom cdm 4705    Fn wfn 5266   -1-1->wf1 5268
This theorem is referenced by:  fun11iun  5509  fnwelem  6246  tposf12  6275  fodomr  7028  domssex  7038  acndom  7694  acndom2  7697  ackbij1b  7881  fin1a2lem6  8047  cnt0  17090  cnt1  17094  cnhaus  17098  hmeoimaf1o  17477  ctex  23351  rankeq1o  24873  hfninf  24888  eldioph2lem2  26943  uslgra1  28252  usgra1  28253
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 5274  df-f 5275  df-f1 5276
  Copyright terms: Public domain W3C validator