Theorem f1odm 5587

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4725   Fn wfn 5321  –1-1-onto→wf1o 5325

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 5329  df-f 5330  df-f1 5331  df-f1o 5333

This theorem is referenced by:  f1imacnv  5600  f1opw2  6229  en2  6998  xpcomco  7010  mapen  7032  ssenen  7037  phplem4  7041  phplem4on  7054  dif1en  7068  fiintim  7123  caseinl  7290  caseinr  7291  ctssdccl  7310  fihasheqf1oi  11050  hashfacen  11101  fisumss  11958