Theorem f1odm 6665

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

Syntax hints:   → wi 4   = wceq 1543  dom cdm 5551   Fn wfn 6375  –1-1-onto→wf1o 6379

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 210  df-an 400  df-fn 6383  df-f 6384  df-f1 6385  df-f1o 6387

This theorem is referenced by:  f1imacnv  6677  f1opw2  7460  xpcomco  8735  domss2  8805  mapen  8810  ssenen  8820  phplem4  8828  php3  8832  f1opwfi  8980  unxpwdom2  9204  cnfcomlem  9314  djuun  9542  ackbij2lem2  9854  ackbij2lem3  9855  fin4en1  9923  enfin2i  9935  hashfacenOLD  14019  gsumpropd2lem  18151  symgfixf1  18829  f1omvdmvd  18835  f1omvdconj  18838  pmtrfb  18857  symggen  18862  symggen2  18863  psgnunilem1  18885  basqtop  22608  reghmph  22690  nrmhmph  22691  indishmph  22695  ordthmeolem  22698  ufldom  22859  tgpconncompeqg  23009  imasf1oxms  23387  icchmeo  23838  dvcvx  24917  dvloglem  25536  f1ocnt  30843  cycpmconjvlem  31127  cycpmconjslem2  31141  madjusmdetlem2  31492  madjusmdetlem4  31494  tpr2rico  31576  ballotlemrv  32198  reprpmtf1o  32318  hgt750lemg  32346  subfacp1lem2b  32856  subfacp1lem5  32859  poimirlem3  35517  ismtyres  35703  eldioph2lem1  40285  lnmlmic  40616  ntrclsiex  41340  ntrneiiex  41363  ssnnf1octb  42406  f1oresf1o  44454