Theorem f1odm 5578

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4719   Fn wfn 5313  –1-1-onto→wf1o 5317

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 5321  df-f 5322  df-f1 5323  df-f1o 5325

This theorem is referenced by:  f1imacnv  5591  f1opw2  6218  en2  6981  xpcomco  6993  mapen  7015  ssenen  7020  phplem4  7024  phplem4on  7037  dif1en  7049  fiintim  7101  caseinl  7266  caseinr  7267  ctssdccl  7286  fihasheqf1oi  11017  hashfacen  11066  fisumss  11911