Theorem f1odm 6778

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

Syntax hints:   → wi 4   = wceq 1547  dom cdm 5625   Fn wfn 6487  –1-1-onto→wf1o 6491

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 208  df-an 397  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1imacnv  6790  f1ounsn  7223  f1opw2  7618  xpcomco  9002  domss2  9071  mapen  9076  ssenen  9086  phplem2  9136  php3  9140  f1opwfi  9263  unxpwdom2  9500  cnfcomlem  9618  djuun  9848  ackbij2lem2  10159  ackbij2lem3  10160  fin4en1  10229  enfin2i  10241  gsumpropd2lem  18645  symgfixf1  19410  f1omvdmvd  19416  f1omvdconj  19419  pmtrfb  19438  symggen  19443  symggen2  19444  psgnunilem1  19466  basqtop  23701  reghmph  23783  nrmhmph  23784  indishmph  23788  ordthmeolem  23791  ufldom  23952  tgpconncompeqg  24102  imasf1oxms  24479  icchmeo  24933  dvcvx  26012  dvloglem  26637  f1ocnt  32899  cycpmconjvlem  33229  cycpmconjslem2  33243  madjusmdetlem2  34019  madjusmdetlem4  34021  tpr2rico  34103  ballotlemrv  34711  reprpmtf1o  34817  hgt750lemg  34845  vonf1owev  35343  subfacp1lem2b  35416  subfacp1lem5  35419  poimirlem3  37997  ismtyres  38182  eldioph2lem1  43216  lnmlmic  43540  ntrclsiex  44504  ntrneiiex  44527  ssnnf1octb  45648  f1oresf1o  47760  grimuhgr  48385  isubgr3stgrlem3  48466