Theorem f1odm 5641

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

Syntax hints:   → wi 4   = wceq 1402  dom cdm 4772   Fn wfn 5370  –1-1-onto→wf1o 5374

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 5378  df-f 5379  df-f1 5380  df-f1o 5382

This theorem is referenced by:  f1imacnv  5654  f1opw2  6290  en2  7106  xpcomco  7118  mapen  7140  ssenen  7146  phplem4  7150  phplem4on  7163  dif1en  7177  fiintim  7232  caseinl  7425  caseinr  7426  ctssdccl  7445  fihasheqf1oi  11209  hashfacen  11267  fisumss  12142  ballotfilemrv  13246