Theorem f1f 6775

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 6542	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 502	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5658  Fun wfun 6531  ⟶wf 6533  –1-1→wf1 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1 6542

This theorem is used by:  f1fn  6776  f1rel  6779  f1ss  6782  f1ssres  6784  f1co  6788  f1of  6821  dff1o5  6831  f1un  6842  fsnd  6866  f1cofveqaeq  7258  f1cofveqaeqALT  7259  2f1fvneq  7261  f1dom3el3dif  7270  f1cdmsn  7287  f1prex  7289  cocan1  7296  fvf1pr  7312  f1we  7360  f1iun  7945  f1dmex  7958  f1o2ndf1  8123  oacomf1olem  8555  brdomg  8968  f1dom2g  8979  f1domg  8981  dom3d  9004  f1imaen2g  9025  2dom  9041  domdifsn  9062  xpdom2  9074  domunsncan  9079  dom0  9107  fodomr  9130  domss2  9138  domssex2  9139  f1domfi  9179  sucdom2  9201  f1finf1o  9247  infn0  9276  f1fi  9288  fodomfir  9301  oiexg  9511  hartogslem1  9518  infdifsn  9640  fseqenlem1  10031  fseqenlem2  10032  acndom  10058  acndom2  10061  dfac12lem2  10151  dfac12lem3  10152  ackbij1  10243  fictb  10250  cfsmolem  10276  cfcoflem  10278  cfcof  10280  fin23lem17  10344  fin23lem32  10350  fin23lem39  10356  fin23lem41  10358  fin1a2lem6  10411  fin1a2lem7  10412  iundom2g  10552  alephreg  10595  canthnumlem  10661  canthwelem  10663  pwfseqlem1  10671  pwfseqlem5  10676  fvf1tp  13854  seqf1olem1  14109  hashf1rn  14420  hashimarn  14509  hashf1dmcdm  14513  hashf1lem1  14524  hashf1lem2  14525  cshf1  14885  setcmon  18182  injsubmefmnd  19012  odinf  19696  odcl2  19698  sylow1lem2  19732  gsumval3lem1  20038  gsumval3lem2  20039  gsumval3  20040  gsumzcl2  20043  gsumzf1o  20045  gsumzaddlem  20054  gsumzmhm  20070  gsumzoppg  20077  dprdf1  20168  f1lindf  22041  f1linds  22044  lindfmm  22046  mdetunilem8  22847  2ndcdisj  23688  itg1addlem4  25933  reeff1o  26690  birthdaylem1  27196  dchrisum0fno1  27755  ushgruhgr  29534  umgr0e  29575  usgredgss  29627  ausgrusgrb  29633  usgrss  29642  uspgrupgr  29646  usgrumgr  29649  usgruspgrb  29651  usgrislfuspgr  29655  usgredg2ALT  29661  ushgredgedg  29697  ushgredgedgloop  29699  usgr2pth  30237  0wlkons1  30599  trlsegvdeg  30715  fsumiunle  33307  cycpmco2lem1  33574  cycpmco2lem5  33578  cycpmco2  33581  cycpmconjv  33590  cyc3conja  33605  idomsubr  33758  islbs5  33821  extdgfialglem1  34210  qqhre  34538  esumiun  34612  vonf1wev  35713  erdszelem4  35781  erdszelem8  35785  erdszelem9  35786  erdsze2lem2  35791  mh-inf3f1  37168  pibt2  38179  aks6d1c2  43004  aks6d1c6lem3  43046  diophrw  43612  eldioph2lem2  43614  eldioph2  43615  eldioph2b  43616  cantnfub2  44171  seff  45141  fargshiftf1  48349  fmtnoinf  48447  upgrimtrlslem2  48829  ushggricedg  48851  grtrimap  48872  oppff1o  50083  fucoppcid  50342  diag1f1o  50468  diag2f1o  50471