Theorem f1dm 6735

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Wolf Lammen, 29-May-2024.)

Assertion

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

Proof of Theorem f1dm

Step	Hyp	Ref	Expression
1		f1fn 6732	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6598	1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5625  –1-1→wf1 6490

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 207  df-an 396  df-fn 6496  df-f 6497  df-f1 6498

This theorem is referenced by:  f1iun  7891  fnwelem  8076  tposf12  8196  fodomr  9061  domssex  9071  fodomfir  9233  f1dmvrnfibi  9246  f1vrnfibi  9247  acndom  9966  acndom2  9969  ackbij1b  10153  fin1a2lem6  10320  hashf1dmrn  14371  cnt0  23295  cnt1  23299  cnhaus  23303  hmeoimaf1o  23719  uspgr1e  29322  s2f1  33030  lindflbs  33464  fineqvinfep  35294  rankeq1o  36378  hfninf  36393  eldioph2lem2  43081