Theorem f1odm 6612

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

Syntax hints:   → wi 4   = wceq 1531  dom cdm 5548   Fn wfn 6343  –1-1-onto→wf1o 6347

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 6351  df-f 6352  df-f1 6353  df-f1o 6355

This theorem is referenced by:  f1imacnv  6624  f1opw2  7392  xpcomco  8599  domss2  8668  mapen  8673  ssenen  8683  phplem4  8691  php3  8695  f1opwfi  8820  unxpwdom2  9044  cnfcomlem  9154  djuun  9347  ackbij2lem2  9654  ackbij2lem3  9655  fin4en1  9723  enfin2i  9735  hashfacen  13804  gsumpropd2lem  17881  symgfixf1  18557  f1omvdmvd  18563  f1omvdconj  18566  pmtrfb  18585  symggen  18590  symggen2  18591  psgnunilem1  18613  basqtop  22311  reghmph  22393  nrmhmph  22394  indishmph  22398  ordthmeolem  22401  ufldom  22562  tgpconncompeqg  22712  imasf1oxms  23091  icchmeo  23537  dvcvx  24609  dvloglem  25223  f1ocnt  30517  cycpmconjvlem  30776  cycpmconjslem2  30790  madjusmdetlem2  31086  madjusmdetlem4  31088  tpr2rico  31148  ballotlemrv  31770  reprpmtf1o  31890  hgt750lemg  31918  subfacp1lem2b  32421  subfacp1lem5  32424  poimirlem3  34887  ismtyres  35078  eldioph2lem1  39347  lnmlmic  39678  ntrclsiex  40393  ntrneiiex  40416  ssnnf1octb  41445  f1oresf1o  43479