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

Theorem f1of 5069
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of (𝐹:A1-1-ontoB𝐹:AB)

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 5068 . 2 (𝐹:A1-1-ontoB𝐹:A1-1B)
2 f1f 5035 . 2 (𝐹:A1-1B𝐹:AB)
31, 2syl 14 1 (𝐹:A1-1-ontoB𝐹:AB)
Colors of variables: wff set class
Syntax hints:  wi 4  wf 4841  1-1wf1 4842  1-1-ontowf1o 4844
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 4850  df-f1o 4852
This theorem is referenced by:  f1ofn  5070  f1oabexg  5081  f1ompt  5263  f1oresrab  5272  fsn  5278  fsnunf  5305  f1ocnvfv1  5360  f1ocnvfv2  5361  f1ocnvdm  5364  fcof1o  5372  isocnv  5394  isores2  5396  isotr  5399  isopolem  5404  isosolem  5406  f1oiso2  5409  f1ofveu  5443  smoiso  5858  f1oen2g  6171  en1  6215  enm  6230  cnrecnv  9118
  Copyright terms: Public domain W3C validator