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

Theorem f1of 5126
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 5125 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 5092 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wf 4898  1-1wf1 4899  1-1-ontowf1o 4901
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-f1 4907  df-f1o 4909
This theorem is referenced by:  f1ofn  5127  f1oabexg  5138  f1ompt  5320  f1oresrab  5329  fsn  5335  fsnunf  5362  f1ocnvfv1  5417  f1ocnvfv2  5418  f1ocnvdm  5421  fcof1o  5429  isocnv  5451  isores2  5453  isotr  5456  isopolem  5461  isosolem  5463  f1oiso2  5466  f1ofveu  5500  smoiso  5917  f1oen2g  6235  en1  6279  enm  6294  fidceq  6330  dif1en  6337  fin0  6342  fin0or  6343  ac6sfi  6352  ordiso2  6357  cnrecnv  9510
  Copyright terms: Public domain W3C validator