Theorem f1odm 5643

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4774   Fn wfn 5372  –1-1-onto→wf1o 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381  df-f1 5382  df-f1o 5384

This theorem is used by:  f1imacnv  5656  f1opw2  6296  en2  7112  xpcomco  7124  mapen  7146  ssenen  7152  phplem4  7156  phplem4on  7169  dif1en  7183  fiintim  7238  caseinl  7432  caseinr  7433  ctssdccl  7452  fihasheqf1oi  11241  hashfacen  11299  fisumss  12177  ballotfilemrv  13314