Theorem f1odm 6141

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

Syntax hints:   → wi 4   = wceq 1483  dom cdm 5114   Fn wfn 5883  –1-1-onto→wf1o 5887

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 386  df-fn 5891  df-f 5892  df-f1 5893  df-f1o 5895

This theorem is referenced by:  f1imacnv  6153  f1opw2  6888  xpcomco  8050  domss2  8119  mapen  8124  ssenen  8134  phplem4  8142  php3  8146  f1opwfi  8270  unxpwdom2  8493  cnfcomlem  8596  ackbij2lem2  9062  ackbij2lem3  9063  fin4en1  9131  enfin2i  9143  hashfacen  13238  gsumpropd2lem  17273  symgbas  17800  symgfixf1  17857  f1omvdmvd  17863  f1omvdconj  17866  pmtrfb  17885  symggen  17890  symggen2  17891  psgnunilem1  17913  basqtop  21514  reghmph  21596  nrmhmph  21597  indishmph  21601  ordthmeolem  21604  ufldom  21766  tgpconncompeqg  21915  imasf1oxms  22294  icchmeo  22740  dvcvx  23783  dvloglem  24394  f1ocnt  29559  madjusmdetlem2  29894  madjusmdetlem4  29896  tpr2rico  29958  ballotlemrv  30581  reprpmtf1o  30704  hgt750lemg  30732  subfacp1lem2b  31163  subfacp1lem5  31166  poimirlem3  33412  ismtyres  33607  eldioph2lem1  37323  lnmlmic  37658  ntrclsiex  38351  ntrneiiex  38374  ssnnf1octb  39382