MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f1o Unicode version

Definition df-f1o 5600
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5826, dff1o3 5827, dff1o4 5829, and dff1o5 5830. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1o

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3
41, 2, 3wf1o 5592 . 2
51, 2, 3wf1 5590 . . 3
61, 2, 3wfo 5591 . . 3
75, 6wa 369 . 2
84, 7wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  f1oeq1  5812  f1oeq2  5813  f1oeq3  5814  nff1o  5819  f1of1  5820  dff1o2  5826  dff1o5  5830  f1oco  5843  fo00  5854  dff1o6  6181  nvof1o  6186  fcof1od  6197  soisoi  6224  f1oweALT  6784  tposf1o2  7000  smoiso2  7059  f1finf1o  7766  unfilem2  7805  fofinf1o  7821  alephiso  8500  cnref1o  11244  wwlktovf1o  12897  1arith  14445  xpsff1o  14965  isffth2  15285  ffthf1o  15288  orbsta  16351  symgextf1o  16448  symgfixf1o  16465  odf1o1  16592  znf1o  18590  cygznlem3  18608  scmatf1o  19034  m2cpmf1o  19258  pm2mpf1o  19316  reeff1o  22842  recosf1o  22922  efif1olem4  22932  dvdsmulf1o  23470  wlknwwlknbij  24713  wlkiswwlkbij  24720  wwlkextbij0  24732  clwwlkf1o  24798  clwlkf1oclwwlk  24851  eupatrl  24968  frgrancvvdeqlem8  25040  numclwlk1lem2f1o  25096  unopf1o  26835  ghomf1olem  29034  sumnnodd  31636  dvnprodlem1  31743  fourierdlem54  31943
  Copyright terms: Public domain W3C validator