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

Theorem f1of 5154
 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 5153 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 5120 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4  ⟶wf 4926  –1-1→wf1 4927  –1-1-onto→wf1o 4929 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103 This theorem depends on definitions:  df-bi 114  df-f1 4935  df-f1o 4937 This theorem is referenced by:  f1ofn  5155  f1oabexg  5166  f1ompt  5348  f1oresrab  5357  fsn  5363  fsnunf  5390  f1ocnvfv1  5445  f1ocnvfv2  5446  f1ocnvdm  5449  fcof1o  5457  isocnv  5479  isores2  5481  isotr  5484  isopolem  5489  isosolem  5491  f1oiso2  5494  f1ofveu  5528  smoiso  5948  f1oen2g  6266  en1  6310  enm  6325  fidceq  6361  dif1en  6368  fin0  6373  fin0or  6374  ac6sfi  6383  isotilem  6410  supisoex  6413  supisoti  6414  ordiso2  6415  cnrecnv  9738
 Copyright terms: Public domain W3C validator