Theorem f1dm 6821

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 6818	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6684	1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700  –1-1→wf1 6570

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 6576  df-f 6577  df-f1 6578

This theorem is referenced by:  f1iun  7984  fnwelem  8172  tposf12  8292  fodomr  9194  domssex  9204  fodomfir  9396  f1dmvrnfibi  9409  f1vrnfibi  9410  acndom  10120  acndom2  10123  ackbij1b  10307  fin1a2lem6  10474  hashf1dmrn  14492  cnt0  23375  cnt1  23379  cnhaus  23383  hmeoimaf1o  23799  uspgr1e  29279  s2f1  32911  lindflbs  33372  rankeq1o  36135  hfninf  36150  eldioph2lem2  42717