Theorem f1f 6776

Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)

Assertion

Ref	Expression
f1f	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1f

Step	Hyp	Ref	Expression
1		df-f1 6543	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 501	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5662  Fun wfun 6532  ⟶wf 6534  –1-1→wf1 6535

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 401  df-f1 6543

This theorem is referenced by:  f1fn  6777  f1rel  6780  f1ss  6783  f1ssres  6785  f1co  6789  f1of  6822  dff1o5  6832  f1un  6843  fsnd  6867  f1cofveqaeq  7257  f1cofveqaeqALT  7258  2f1fvneq  7260  f1dom3el3dif  7269  f1cdmsn  7282  f1prex  7284  cocan1  7291  fvf1pr  7307  f1iun  7942  f1dmex  7955  f1o2ndf1  8118  oacomf1olem  8550  brdomg  8956  f1dom2g  8967  f1domg  8969  dom3d  8992  f1imaen2g  9013  2dom  9028  domdifsn  9049  xpdom2  9061  domunsncan  9066  dom0  9094  fodomr  9117  domss2  9125  domssex2  9126  f1domfi  9166  sucdom2  9188  f1finf1o  9234  infn0  9263  f1fi  9275  fodomfir  9288  oiexg  9498  hartogslem1  9505  infdifsn  9627  fseqenlem1  10009  fseqenlem2  10010  ac10ct  10019  acndom  10036  acndom2  10039  dfac12lem2  10129  dfac12lem3  10130  ackbij1  10221  fictb  10228  cfsmolem  10255  cfcoflem  10257  cfcof  10259  fin23lem17  10323  fin23lem32  10329  fin23lem39  10335  fin23lem41  10337  fin1a2lem6  10390  fin1a2lem7  10391  iundom2g  10525  alephreg  10568  canthnumlem  10634  canthwelem  10636  pwfseqlem1  10644  pwfseqlem5  10649  fvf1tp  13824  seqf1olem1  14079  hashf1rn  14390  hashimarn  14479  hashf1dmcdm  14483  hashf1lem1  14494  hashf1lem2  14495  cshf1  14849  setcmon  18145  injsubmefmnd  18957  odinf  19634  odcl2  19636  sylow1lem2  19670  gsumval3lem1  19976  gsumval3lem2  19977  gsumval3  19978  gsumzcl2  19981  gsumzf1o  19983  gsumzaddlem  19992  gsumzmhm  20008  gsumzoppg  20015  dprdf1  20106  f1lindf  21953  f1linds  21956  lindfmm  21958  mdetunilem8  22757  2ndcdisj  23594  itg1addlem4  25839  reeff1o  26588  birthdaylem1  27094  dchrisum0fno1  27653  ushgruhgr  29397  umgr0e  29438  usgredgss  29487  ausgrusgrb  29493  usgrss  29502  uspgrupgr  29506  usgrumgr  29509  usgruspgrb  29511  usgrislfuspgr  29515  usgredg2ALT  29521  ushgredgedg  29557  ushgredgedgloop  29559  usgr2pth  30091  0wlkons1  30450  trlsegvdeg  30556  fsumiunle  33151  cycpmco2lem1  33424  cycpmco2lem5  33428  cycpmco2  33431  cycpmconjv  33440  cyc3conja  33455  idomsubr  33608  islbs5  33671  extdgfialglem1  34060  qqhre  34388  esumiun  34462  vonf1wev  35570  erdszelem4  35664  erdszelem8  35668  erdszelem9  35669  erdsze2lem2  35674  mh-inf3f1  37030  pibt2  38041  aks6d1c2  42875  aks6d1c6lem3  42917  diophrw  43470  eldioph2lem2  43472  eldioph2  43473  eldioph2b  43474  dnwech  43755  cantnfub2  44029  seff  44999  fargshiftf1  48167  fmtnoinf  48265  upgrimtrlslem2  48647  ushggricedg  48669  grtrimap  48690  oppff1o  49904  fucoppcid  50163  diag1f1o  50289  diag2f1o  50292