Theorem f1odm 6179

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

Syntax hints:   → wi 4   = wceq 1523  dom cdm 5143   Fn wfn 5921  –1-1-onto→wf1o 5925

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 197  df-an 385  df-fn 5929  df-f 5930  df-f1 5931  df-f1o 5933

This theorem is referenced by:  f1imacnv  6191  f1opw2  6930  xpcomco  8091  domss2  8160  mapen  8165  ssenen  8175  phplem4  8183  php3  8187  f1opwfi  8311  unxpwdom2  8534  cnfcomlem  8634  ackbij2lem2  9100  ackbij2lem3  9101  fin4en1  9169  enfin2i  9181  hashfacen  13276  gsumpropd2lem  17320  symgbas  17846  symgfixf1  17903  f1omvdmvd  17909  f1omvdconj  17912  pmtrfb  17931  symggen  17936  symggen2  17937  psgnunilem1  17959  basqtop  21562  reghmph  21644  nrmhmph  21645  indishmph  21649  ordthmeolem  21652  ufldom  21813  tgpconncompeqg  21962  imasf1oxms  22341  icchmeo  22787  dvcvx  23828  dvloglem  24439  f1ocnt  29687  madjusmdetlem2  30022  madjusmdetlem4  30024  tpr2rico  30086  ballotlemrv  30709  reprpmtf1o  30832  hgt750lemg  30860  subfacp1lem2b  31289  subfacp1lem5  31292  poimirlem3  33542  ismtyres  33737  eldioph2lem1  37640  lnmlmic  37975  ntrclsiex  38668  ntrneiiex  38691  ssnnf1octb  39696