Theorem f1odm 5581

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4720   Fn wfn 5316  –1-1-onto→wf1o 5320

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 5324  df-f 5325  df-f1 5326  df-f1o 5328

This theorem is referenced by:  f1imacnv  5594  f1opw2  6221  en2  6986  xpcomco  6998  mapen  7020  ssenen  7025  phplem4  7029  phplem4on  7042  dif1en  7054  fiintim  7109  caseinl  7274  caseinr  7275  ctssdccl  7294  fihasheqf1oi  11026  hashfacen  11076  fisumss  11924