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

Theorem f1dm 6808
Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Wolf Lammen, 29-May-2024.)
Assertion
Ref Expression
f1dm (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1dm
StepHypRef Expression
1 f1fn 6805 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
21fndmd 6673 1 (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  dom cdm 5685  1-1wf1 6558
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 207  df-an 396  df-fn 6564  df-f 6565  df-f1 6566
This theorem is referenced by:  f1iun  7968  fnwelem  8156  tposf12  8276  fodomr  9168  domssex  9178  fodomfir  9368  f1dmvrnfibi  9381  f1vrnfibi  9382  acndom  10091  acndom2  10094  ackbij1b  10278  fin1a2lem6  10445  hashf1dmrn  14482  cnt0  23354  cnt1  23358  cnhaus  23362  hmeoimaf1o  23778  uspgr1e  29261  s2f1  32929  lindflbs  33407  rankeq1o  36172  hfninf  36187  eldioph2lem2  42772
  Copyright terms: Public domain W3C validator