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

Theorem f1f 5999
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 5795 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 474 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5027  Fun wfun 5784  wf 5786  1-1wf1 5787
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 195  df-an 384  df-f1 5795
This theorem is referenced by:  f1fn  6000  f1ss  6004  f1ssres  6006  f1of  6035  dff1o5  6044  fsnd  6076  f1dom3el3dif  6404  f1prex  6417  cocan1  6424  fun11iun  6996  f1dmex  7006  f1o2ndf1  7149  oacomf1olem  7508  brdomg  7828  f1dom2g  7836  f1domg  7838  dom3d  7860  f1imaen2g  7880  2dom  7892  domdifsn  7905  xpdom2  7917  domunsncan  7922  fodomr  7973  domss2  7981  domssex2  7982  sucdom2  8018  f1finf1o  8049  f1fi  8113  oiexg  8300  hartogslem1  8307  infdifsn  8414  fseqenlem1  8707  fseqenlem2  8708  ac10ct  8717  acndom  8734  acndom2  8737  dfac12lem2  8826  dfac12lem3  8827  ackbij1  8920  fictb  8927  cfsmolem  8952  cfcoflem  8954  cfcof  8956  fin23lem17  9020  fin23lem32  9026  fin23lem39  9032  fin23lem41  9034  fin1a2lem6  9087  fin1a2lem7  9088  iundom2g  9218  alephreg  9260  canthnumlem  9326  canthwelem  9328  pwfseqlem1  9336  pwfseqlem5  9341  seqf1olem1  12657  hashf1rn  12956  hashf1rnOLD  12957  hashimarn  13037  hashf1lem1  13048  hashf1lem2  13049  cshf1  13353  setcmon  16506  odinf  17749  odcl2  17751  odf1o1  17756  sylow1lem2  17783  gsumval3lem1  18075  gsumval3lem2  18076  gsumval3  18077  gsumzcl2  18080  gsumzf1o  18082  gsumzaddlem  18090  gsumzmhm  18106  gsumzoppg  18113  dprdf1  18201  f1lindf  19922  f1linds  19925  lindfmm  19927  mdetunilem8  20186  2ndcdisj  21011  itg1addlem4  23189  reeff1o  23922  birthdaylem1  24395  basellem3  24526  dchrisum0fno1  24917  ushgrauhgra  25598  edgss  25647  ausisusgra  25650  usgrass  25656  uslisumgra  25659  usgra0v  25666  usgraedg2  25670  usgraedgrnv  25672  usgrarnedg  25679  usgraedg4  25682  usgra1v  25685  usgrares1  25705  cusgrarn  25754  fargshiftf1  25931  usgrcyclnl2  25935  clwlkisclwwlklem1  26081  usgravd00  26212  qqhre  29198  esumiun  29289  erdszelem4  30236  erdszelem8  30240  erdszelem9  30241  erdsze2lem2  30246  diophrw  36136  eldioph2lem2  36138  eldioph2  36139  eldioph2b  36140  dnwech  36432  seff  37326  fmtnoinf  39784  2f1fvneq  40131  f1cofveqaeq  40132  f1cofveqaeqALT  40133  ushgruhgr  40286  umgr0e  40330  usgredgss  40385  ausgrusgrb  40390  usgrss  40399  uspgrupgr  40401  usgrumgr  40404  usgruspgrb  40406  usgrislfuspgr  40409  usgredg2ALT  40415  ushgredgedga  40451  ushgredgedgaloop  40453  usgr2pth  40965  0wlkOns1  41284  trlsegvdeg  41390
  Copyright terms: Public domain W3C validator