Theorem f1odm 6621

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5557   Fn wfn 6352  –1-1-onto→wf1o 6356

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 209  df-an 399  df-fn 6360  df-f 6361  df-f1 6362  df-f1o 6364

This theorem is referenced by:  f1imacnv  6633  f1opw2  7402  xpcomco  8609  domss2  8678  mapen  8683  ssenen  8693  phplem4  8701  php3  8705  f1opwfi  8830  unxpwdom2  9054  cnfcomlem  9164  djuun  9357  ackbij2lem2  9664  ackbij2lem3  9665  fin4en1  9733  enfin2i  9745  hashfacen  13815  gsumpropd2lem  17891  symgfixf1  18567  f1omvdmvd  18573  f1omvdconj  18576  pmtrfb  18595  symggen  18600  symggen2  18601  psgnunilem1  18623  basqtop  22321  reghmph  22403  nrmhmph  22404  indishmph  22408  ordthmeolem  22411  ufldom  22572  tgpconncompeqg  22722  imasf1oxms  23101  icchmeo  23547  dvcvx  24619  dvloglem  25233  f1ocnt  30527  cycpmconjvlem  30785  cycpmconjslem2  30799  madjusmdetlem2  31095  madjusmdetlem4  31097  tpr2rico  31157  ballotlemrv  31779  reprpmtf1o  31899  hgt750lemg  31927  subfacp1lem2b  32430  subfacp1lem5  32433  poimirlem3  34897  ismtyres  35088  eldioph2lem1  39364  lnmlmic  39695  ntrclsiex  40410  ntrneiiex  40433  ssnnf1octb  41463  f1oresf1o  43496