Theorem f1odm 6852

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

Syntax hints:   → wi 4   = wceq 1536  dom cdm 5688   Fn wfn 6557  –1-1-onto→wf1o 6561

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 6565  df-f 6566  df-f1 6567  df-f1o 6569

This theorem is referenced by:  f1imacnv  6864  f1ounsn  7291  f1opw2  7687  xpcomco  9100  domss2  9174  mapen  9179  ssenen  9189  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  f1opwfi  9393  unxpwdom2  9625  cnfcomlem  9736  djuun  9963  ackbij2lem2  10276  ackbij2lem3  10277  fin4en1  10346  enfin2i  10358  gsumpropd2lem  18704  symgfixf1  19469  f1omvdmvd  19475  f1omvdconj  19478  pmtrfb  19497  symggen  19502  symggen2  19503  psgnunilem1  19525  basqtop  23734  reghmph  23816  nrmhmph  23817  indishmph  23821  ordthmeolem  23824  ufldom  23985  tgpconncompeqg  24135  imasf1oxms  24517  icchmeo  24984  icchmeoOLD  24985  dvcvx  26073  dvloglem  26704  f1ocnt  32809  cycpmconjvlem  33143  cycpmconjslem2  33157  madjusmdetlem2  33788  madjusmdetlem4  33790  tpr2rico  33872  ballotlemrv  34500  reprpmtf1o  34619  hgt750lemg  34647  subfacp1lem2b  35165  subfacp1lem5  35168  poimirlem3  37609  ismtyres  37794  eldioph2lem1  42747  lnmlmic  43076  ntrclsiex  44042  ntrneiiex  44065  ssnnf1octb  45136  f1oresf1o  47239  grimuhgr  47815  isubgr3stgrlem3  47870