Theorem f1f 6756

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

Syntax hints:   → wi 4  ^◡ccnv 5644  Fun wfun 6511  ⟶wf 6513  –1-1→wf1 6514

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 400  df-f1 6522

This theorem is referenced by:  f1fn  6757  f1rel  6760  f1ss  6763  f1ssres  6765  f1co  6769  f1of  6802  dff1o5  6812  f1un  6823  fsnd  6847  f1cofveqaeq  7237  f1cofveqaeqALT  7238  2f1fvneq  7240  f1dom3el3dif  7249  f1cdmsn  7262  f1prex  7264  cocan1  7271  fvf1pr  7287  f1iun  7921  f1dmex  7934  f1o2ndf1  8096  oacomf1olem  8528  brdomg  8935  f1dom2g  8946  f1domg  8948  dom3d  8971  f1imaen2g  8992  2dom  9007  domdifsn  9028  xpdom2  9040  domunsncan  9045  dom0  9073  fodomr  9096  domss2  9104  domssex2  9105  f1domfi  9145  sucdom2  9167  f1finf1o  9213  infn0  9242  f1fi  9254  fodomfir  9268  oiexg  9480  hartogslem1  9487  infdifsn  9609  fseqenlem1  9977  fseqenlem2  9978  ac10ct  9987  acndom  10004  acndom2  10007  dfac12lem2  10098  dfac12lem3  10099  ackbij1  10190  fictb  10197  cfsmolem  10224  cfcoflem  10226  cfcof  10228  fin23lem17  10292  fin23lem32  10298  fin23lem39  10304  fin23lem41  10306  fin1a2lem6  10359  fin1a2lem7  10360  iundom2g  10494  alephreg  10537  canthnumlem  10603  canthwelem  10605  pwfseqlem1  10613  pwfseqlem5  10618  fvf1tp  13796  seqf1olem1  14051  hashf1rn  14362  hashimarn  14450  hashf1dmcdm  14454  hashf1lem1  14465  hashf1lem2  14466  cshf1  14820  setcmon  18103  injsubmefmnd  18914  odinf  19586  odcl2  19588  sylow1lem2  19622  gsumval3lem1  19928  gsumval3lem2  19929  gsumval3  19930  gsumzcl2  19933  gsumzf1o  19935  gsumzaddlem  19944  gsumzmhm  19960  gsumzoppg  19967  dprdf1  20058  f1lindf  21854  f1linds  21857  lindfmm  21859  mdetunilem8  22659  2ndcdisj  23496  itg1addlem4  25741  reeff1o  26487  birthdaylem1  26993  dchrisum0fno1  27552  ushgruhgr  29216  umgr0e  29257  usgredgss  29306  ausgrusgrb  29312  usgrss  29321  uspgrupgr  29325  usgrumgr  29328  usgruspgrb  29330  usgrislfuspgr  29334  usgredg2ALT  29340  ushgredgedg  29376  ushgredgedgloop  29378  usgr2pth  29910  0wlkons1  30269  trlsegvdeg  30375  fsumiunle  32981  cycpmco2lem1  33267  cycpmco2lem5  33271  cycpmco2  33274  cycpmconjv  33283  cyc3conja  33298  idomsubr  33457  islbs5  33527  extdgfialglem1  33950  qqhre  34278  esumiun  34352  vonf1wev  35415  erdszelem4  35508  erdszelem8  35512  erdszelem9  35513  erdsze2lem2  35518  mh-inf3f1  36865  pibt2  37875  aks6d1c2  42711  aks6d1c6lem3  42753  diophrw  43304  eldioph2lem2  43306  eldioph2  43307  eldioph2b  43308  dnwech  43589  cantnfub2  43863  seff  44849  fargshiftf1  48011  fmtnoinf  48109  upgrimtrlslem2  48491  ushggricedg  48513  grtrimap  48534  oppff1o  49734  fucoppcid  49993  diag1f1o  50119  diag2f1o  50122