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

Theorem f1dm 6018
Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1dm (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1dm
StepHypRef Expression
1 f1fn 6015 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fndm 5904 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  dom cdm 5038   Fn wfn 5799  1-1wf1 5801
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 196  df-an 385  df-fn 5807  df-f 5808  df-f1 5809
This theorem is referenced by:  fun11iun  7019  fnwelem  7179  tposf12  7264  ctex  7856  fodomr  7996  domssex  8006  f1dmvrnfibi  8133  f1vrnfibi  8134  acndom  8757  acndom2  8760  ackbij1b  8944  fin1a2lem6  9110  cnt0  20960  cnt1  20964  cnhaus  20968  hmeoimaf1o  21383  uslgra1  25901  usgra1  25902  rankeq1o  31448  hfninf  31463  eldioph2lem2  36342  uspgr1e  40470
  Copyright terms: Public domain W3C validator