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 1528  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 208  df-an 397  df-fn 6351  df-f 6352  df-f1 6353
This theorem is referenced by:  f1iun  7634  fnwelem  7814  tposf12  7906  fodomr  8656  domssex  8666  f1dmvrnfibi  8796  f1vrnfibi  8797  acndom  9465  acndom2  9468  ackbij1b  9649  fin1a2lem6  9815  cnt0  21882  cnt1  21886  cnhaus  21890  hmeoimaf1o  22306  uspgr1e  26953  s2f1  30548  lindflbs  30867  hashf1dmrn  32252  rankeq1o  33529  hfninf  33544  eldioph2lem2  39236
  Copyright terms: Public domain W3C validator