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

Definition df-f1o 5508
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5726, dff1o3 5727, dff1o4 5729, and dff1o5 5730. 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 5500 . 2
51, 2, 3wf1 5498 . . 3
61, 2, 3wfo 5499 . . 3
75, 6wa 360 . 2
84, 7wb 178 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5712  f1oeq2  5713  f1oeq3  5714  nff1o  5719  f1of1  5720  dff1o2  5726  dff1o5  5730  f1oco  5745  fo00  5758  dff1o6  6061  fcof1o  6074  soisoi  6096  f1oweALT  6122  tposf1o2  6555  smoiso2  6680  f1finf1o  7384  unfilem2  7421  fofinf1o  7436  alephiso  8030  cnref1o  10658  1arith  13346  xpsff1o  13844  isffth2  14164  ffthf1o  14167  orbsta  15141  odf1o1  15257  znf1o  16883  cygznlem3  16901  reeff1o  20414  recosf1o  20488  efif1olem4  20498  dvdsmulf1o  21030  eupatrl  21741  unopf1o  23470  nvof1o  24088  ghomf1olem  25209  frgrancvvdeqlem8  28667
  Copyright terms: Public domain W3C validator