Theorem f1dm 6772

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5647  –1-1→wf1 6524

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6530  df-f 6531  df-f1 6532

This theorem is used by:  f1iun  7939  fnwelem  8126  tposf12  8246  fodomr  9125  domssex  9135  fodomfir  9297  f1dmvrnfibi  9308  f1vrnfibi  9309  acndom  10101  acndom2  10104  ackbij1b  10287  fin1a2lem6  10454  hashf1dmrn  14555  cnt0  23625  cnt1  23629  cnhaus  23633  hmeoimaf1o  24050  uspgr1e  29758  s2f1  33443  lindflbs  33867  fineqvinfep  35718  vonf1wev  35812  rankeq1o  36854  hfninf  36857  eldioph2lem2  43710