MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1f Structured version   Visualization version   GIF version

Theorem f1f 6139
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
StepHypRef Expression
1 df-f1 5931 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 475 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5142  Fun wfun 5920  wf 5922  1-1wf1 5923
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 197  df-an 385  df-f1 5931
This theorem is referenced by:  f1fn  6140  f1ss  6144  f1ssres  6146  f1of  6175  dff1o5  6184  fsnd  6217  f1cofveqaeq  6555  f1cofveqaeqALT  6556  2f1fvneq  6557  f1dom3el3dif  6566  f1prex  6579  cocan1  6586  fun11iun  7168  f1dmex  7178  f1o2ndf1  7330  oacomf1olem  7689  brdomg  8007  f1dom2g  8015  f1domg  8017  dom3d  8039  f1imaen2g  8058  2dom  8070  domdifsn  8084  xpdom2  8096  domunsncan  8101  fodomr  8152  domss2  8160  domssex2  8161  sucdom2  8197  f1finf1o  8228  f1fi  8294  oiexg  8481  hartogslem1  8488  infdifsn  8592  fseqenlem1  8885  fseqenlem2  8886  ac10ct  8895  acndom  8912  acndom2  8915  dfac12lem2  9004  dfac12lem3  9005  ackbij1  9098  fictb  9105  cfsmolem  9130  cfcoflem  9132  cfcof  9134  fin23lem17  9198  fin23lem32  9204  fin23lem39  9210  fin23lem41  9212  fin1a2lem6  9265  fin1a2lem7  9266  iundom2g  9400  alephreg  9442  canthnumlem  9508  canthwelem  9510  pwfseqlem1  9518  pwfseqlem5  9523  seqf1olem1  12880  hashf1rn  13181  hashimarn  13265  hashf1lem1  13277  hashf1lem2  13278  cshf1  13602  setcmon  16784  odinf  18026  odcl2  18028  odf1o1  18033  sylow1lem2  18060  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumzmhm  18383  gsumzoppg  18390  dprdf1  18478  f1lindf  20209  f1linds  20212  lindfmm  20214  mdetunilem8  20473  2ndcdisj  21307  itg1addlem4  23511  reeff1o  24246  birthdaylem1  24723  basellem3  24854  dchrisum0fno1  25245  ushgruhgr  26009  umgr0e  26050  usgredgss  26099  ausgrusgrb  26105  usgrss  26114  uspgrupgr  26116  usgrumgr  26119  usgruspgrb  26121  usgrislfuspgr  26124  usgredg2ALT  26130  ushgredgedg  26166  ushgredgedgloop  26168  usgr2pth  26716  0wlkons1  27099  trlsegvdeg  27205  fsumiunle  29703  qqhre  30192  esumiun  30284  erdszelem4  31302  erdszelem8  31306  erdszelem9  31307  erdsze2lem2  31312  diophrw  37639  eldioph2lem2  37641  eldioph2  37642  eldioph2b  37643  dnwech  37935  seff  38825  fargshiftf1  41702  fmtnoinf  41773
  Copyright terms: Public domain W3C validator