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

Theorem f1odm 5446
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 5443 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fndm 5297 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  dom cdm 4611   Fn wfn 5193  1-1-ontowf1o 5197
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 5201  df-f 5202  df-f1 5203  df-f1o 5205
This theorem is referenced by:  f1imacnv  5459  f1opw2  6055  xpcomco  6804  mapen  6824  ssenen  6829  phplem4  6833  phplem4on  6845  dif1en  6857  fiintim  6906  caseinl  7068  caseinr  7069  ctssdccl  7088  fihasheqf1oi  10722  hashfacen  10771  fisumss  11355
  Copyright terms: Public domain W3C validator