Theorem f1odm 6479

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

Syntax hints:   → wi 4   = wceq 1520  dom cdm 5435   Fn wfn 6212  –1-1-onto→wf1o 6216

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 208  df-an 397  df-fn 6220  df-f 6221  df-f1 6222  df-f1o 6224

This theorem is referenced by:  f1imacnv  6491  f1opw2  7249  xpcomco  8444  domss2  8513  mapen  8518  ssenen  8528  phplem4  8536  php3  8540  f1opwfi  8664  unxpwdom2  8888  cnfcomlem  8997  djuun  9190  ackbij2lem2  9497  ackbij2lem3  9498  fin4en1  9566  enfin2i  9578  hashfacen  13648  gsumpropd2lem  17700  symgbas  18227  symgfixf1  18284  f1omvdmvd  18290  f1omvdconj  18293  pmtrfb  18312  symggen  18317  symggen2  18318  psgnunilem1  18340  basqtop  21991  reghmph  22073  nrmhmph  22074  indishmph  22078  ordthmeolem  22081  ufldom  22242  tgpconncompeqg  22391  imasf1oxms  22770  icchmeo  23216  dvcvx  24288  dvloglem  24900  f1ocnt  30181  cycpmconjvlem  30383  cycpmconjslem2  30393  madjusmdetlem2  30664  madjusmdetlem4  30666  tpr2rico  30728  ballotlemrv  31350  reprpmtf1o  31470  hgt750lemg  31498  subfacp1lem2b  31992  subfacp1lem5  31995  poimirlem3  34372  ismtyres  34564  eldioph2lem1  38792  lnmlmic  39124  ntrclsiex  39839  ntrneiiex  39862  ssnnf1octb  40949  f1oresf1o  42959