Theorem f1odm 5572

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

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

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 5317  df-f 5318  df-f1 5319  df-f1o 5321

This theorem is referenced by:  f1imacnv  5585  f1opw2  6202  en2  6963  xpcomco  6973  mapen  6995  ssenen  7000  phplem4  7004  phplem4on  7017  dif1en  7029  fiintim  7081  caseinl  7246  caseinr  7247  ctssdccl  7266  fihasheqf1oi  10996  hashfacen  11045  fisumss  11889