Theorem f1odm 5596

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

Step	Hyp	Ref	Expression
1		f1ofn 5593	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 5436	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4731   Fn wfn 5328  –1-1-onto→wf1o 5332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-fn 5336  df-f 5337  df-f1 5338  df-f1o 5340

This theorem is referenced by:  f1imacnv  5609  f1opw2  6239  en2  7041  xpcomco  7053  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  dif1en  7111  fiintim  7166  caseinl  7333  caseinr  7334  ctssdccl  7353  fihasheqf1oi  11093  hashfacen  11144  fisumss  12014