Theorem f1odm 5584

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 5581	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 5426	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4723   Fn wfn 5319  –1-1-onto→wf1o 5323

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 5327  df-f 5328  df-f1 5329  df-f1o 5331

This theorem is referenced by:  f1imacnv  5597  f1opw2  6224  en2  6993  xpcomco  7005  mapen  7027  ssenen  7032  phplem4  7036  phplem4on  7049  dif1en  7063  fiintim  7118  caseinl  7284  caseinr  7285  ctssdccl  7304  fihasheqf1oi  11042  hashfacen  11093  fisumss  11946