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

Theorem f1dm 6218
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 6215 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fndm 6103 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  dom cdm 5218   Fn wfn 5996  1-1wf1 5998
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 385  df-fn 6004  df-f 6005  df-f1 6006
This theorem is referenced by:  fun11iun  7243  fnwelem  7412  tposf12  7497  ctex  8087  fodomr  8227  domssex  8237  f1dmvrnfibi  8366  f1vrnfibi  8367  acndom  8987  acndom2  8990  ackbij1b  9174  fin1a2lem6  9340  cnt0  21273  cnt1  21277  cnhaus  21281  hmeoimaf1o  21696  uspgr1e  26256  rankeq1o  32505  hfninf  32520  eldioph2lem2  37743
  Copyright terms: Public domain W3C validator