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

Theorem f1dm 6072
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 6069 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fndm 5958 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  dom cdm 5084   Fn wfn 5852  1-1wf1 5854
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 197  df-an 386  df-fn 5860  df-f 5861  df-f1 5862
This theorem is referenced by:  fun11iun  7088  fnwelem  7252  tposf12  7337  ctex  7930  fodomr  8071  domssex  8081  f1dmvrnfibi  8210  f1vrnfibi  8211  acndom  8834  acndom2  8837  ackbij1b  9021  fin1a2lem6  9187  cnt0  21090  cnt1  21094  cnhaus  21098  hmeoimaf1o  21513  uspgr1e  26063  rankeq1o  31973  hfninf  31988  eldioph2lem2  36843
  Copyright terms: Public domain W3C validator