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

Theorem f1dm 6321
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 6318 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fndm 6202 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  dom cdm 5313   Fn wfn 6097  1-1wf1 6099
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 199  df-an 386  df-fn 6105  df-f 6106  df-f1 6107
This theorem is referenced by:  fun11iun  7362  fnwelem  7530  tposf12  7616  ctex  8211  fodomr  8354  domssex  8364  f1dmvrnfibi  8493  f1vrnfibi  8494  acndom  9161  acndom2  9164  ackbij1b  9350  fin1a2lem6  9516  cnt0  21478  cnt1  21482  cnhaus  21486  hmeoimaf1o  21901  uspgr1e  26477  rankeq1o  32790  hfninf  32805  eldioph2lem2  38105
  Copyright terms: Public domain W3C validator