Theorem f1odm 6834

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5675   Fn wfn 6535  –1-1-onto→wf1o 6539

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 206  df-an 397  df-fn 6543  df-f 6544  df-f1 6545  df-f1o 6547

This theorem is referenced by:  f1imacnv  6846  f1opw2  7657  xpcomco  9058  domss2  9132  mapen  9137  ssenen  9147  phplem2  9204  php3  9208  phplem4OLD  9216  php3OLD  9220  f1opwfi  9352  unxpwdom2  9579  cnfcomlem  9690  djuun  9917  ackbij2lem2  10231  ackbij2lem3  10232  fin4en1  10300  enfin2i  10312  hashfacenOLD  14410  gsumpropd2lem  18594  symgfixf1  19299  f1omvdmvd  19305  f1omvdconj  19308  pmtrfb  19327  symggen  19332  symggen2  19333  psgnunilem1  19355  basqtop  23206  reghmph  23288  nrmhmph  23289  indishmph  23293  ordthmeolem  23296  ufldom  23457  tgpconncompeqg  23607  imasf1oxms  23989  icchmeo  24448  dvcvx  25528  dvloglem  26147  f1ocnt  32000  cycpmconjvlem  32287  cycpmconjslem2  32301  madjusmdetlem2  32796  madjusmdetlem4  32798  tpr2rico  32880  ballotlemrv  33506  reprpmtf1o  33626  hgt750lemg  33654  subfacp1lem2b  34160  subfacp1lem5  34163  gg-icchmeo  35158  poimirlem3  36479  ismtyres  36664  eldioph2lem1  41483  lnmlmic  41815  ntrclsiex  42789  ntrneiiex  42812  ssnnf1octb  43878  f1oresf1o  45984