ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1f GIF version

Theorem f1f 5422
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 5222 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 274 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4626  Fun wfun 5211  wf 5213  1-1wf1 5214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-f1 5222
This theorem is referenced by:  f1rn  5423  f1fn  5424  f1ss  5428  f1ssres  5431  f1of  5462  dff1o5  5471  fsnd  5505  cocan1  5788  f1o2ndf1  6229  brdomg  6748  f1dom2g  6756  f1domg  6758  dom3d  6774  f1imaen2g  6793  2dom  6805  xpdom2  6831  dom0  6838  phplem4dom  6862  isinfinf  6897  infm  6904  updjudhcoinlf  7079  updjudhcoinrg  7080  casef1  7089  djudom  7092  difinfsnlem  7098  difinfsn  7099  fihashf1rn  10768  ennnfonelemrn  12420  reeff1o  14197  pwle2  14751
  Copyright terms: Public domain W3C validator