ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1odm GIF version

Theorem f1odm 5418
Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1odm (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1odm
StepHypRef Expression
1 f1ofn 5415 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 5269 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1335  dom cdm 4586   Fn wfn 5165  1-1-ontowf1o 5169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-fn 5173  df-f 5174  df-f1 5175  df-f1o 5177
This theorem is referenced by:  f1imacnv  5431  f1opw2  6026  xpcomco  6771  mapen  6791  ssenen  6796  phplem4  6800  phplem4on  6812  dif1en  6824  fiintim  6873  caseinl  7035  caseinr  7036  ctssdccl  7055  fihasheqf1oi  10662  hashfacen  10707  fisumss  11289
  Copyright terms: Public domain W3C validator