Theorem f1dm 6582

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1dm	⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1dm

Step	Hyp	Ref	Expression
1		f1fn 6579	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6458	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1536  dom cdm 5558   Fn wfn 6353  –1-1→wf1 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-fn 6361  df-f 6362  df-f1 6363

This theorem is referenced by:  f1iun  7648  fnwelem  7828  tposf12  7920  fodomr  8671  domssex  8681  f1dmvrnfibi  8811  f1vrnfibi  8812  acndom  9480  acndom2  9483  ackbij1b  9664  fin1a2lem6  9830  cnt0  21957  cnt1  21961  cnhaus  21965  hmeoimaf1o  22381  uspgr1e  27029  s2f1  30625  lindflbs  30944  hashf1dmrn  32359  rankeq1o  33636  hfninf  33651  eldioph2lem2  39364