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

Theorem f1dm 6572
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 6569 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fndm 6448 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1531  dom cdm 5548   Fn wfn 6343  1-1wf1 6345
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 209  df-an 399  df-fn 6351  df-f 6352  df-f1 6353
This theorem is referenced by:  f1iun  7637  fnwelem  7817  tposf12  7909  fodomr  8660  domssex  8670  f1dmvrnfibi  8800  f1vrnfibi  8801  acndom  9469  acndom2  9472  ackbij1b  9653  fin1a2lem6  9819  cnt0  21946  cnt1  21950  cnhaus  21954  hmeoimaf1o  22370  uspgr1e  27018  s2f1  30614  lindflbs  30933  hashf1dmrn  32348  rankeq1o  33625  hfninf  33640  eldioph2lem2  39348
  Copyright terms: Public domain W3C validator