Theorem f1odm 6704

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580   Fn wfn 6413  –1-1-onto→wf1o 6417

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 206  df-an 396  df-fn 6421  df-f 6422  df-f1 6423  df-f1o 6425

This theorem is referenced by:  f1imacnv  6716  f1opw2  7502  xpcomco  8802  domss2  8872  mapen  8877  ssenen  8887  phplem4  8895  php3  8899  f1opwfi  9053  unxpwdom2  9277  cnfcomlem  9387  djuun  9615  ackbij2lem2  9927  ackbij2lem3  9928  fin4en1  9996  enfin2i  10008  hashfacenOLD  14095  gsumpropd2lem  18278  symgfixf1  18960  f1omvdmvd  18966  f1omvdconj  18969  pmtrfb  18988  symggen  18993  symggen2  18994  psgnunilem1  19016  basqtop  22770  reghmph  22852  nrmhmph  22853  indishmph  22857  ordthmeolem  22860  ufldom  23021  tgpconncompeqg  23171  imasf1oxms  23551  icchmeo  24010  dvcvx  25089  dvloglem  25708  f1ocnt  31025  cycpmconjvlem  31310  cycpmconjslem2  31324  madjusmdetlem2  31680  madjusmdetlem4  31682  tpr2rico  31764  ballotlemrv  32386  reprpmtf1o  32506  hgt750lemg  32534  subfacp1lem2b  33043  subfacp1lem5  33046  poimirlem3  35707  ismtyres  35893  eldioph2lem1  40498  lnmlmic  40829  ntrclsiex  41552  ntrneiiex  41575  ssnnf1octb  42622  f1oresf1o  44669