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

Definition df-f1o 5445
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5663, dff1o3 5664, dff1o4 5666, and dff1o5 5667. 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 5437 . 2
51, 2, 3wf1 5435 . . 3
61, 2, 3wfo 5436 . . 3
75, 6wa 360 . 2
84, 7wb 178 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5649  f1oeq2  5650  f1oeq3  5651  nff1o  5656  f1of1  5657  dff1o2  5663  dff1o5  5667  f1oco  5680  fo00  5691  dff1o6  5994  fcof1o  6007  soisoi  6029  f1oweALT  6567  tposf1o2  6737  smoiso2  6793  f1finf1o  7500  unfilem2  7538  fofinf1o  7553  alephiso  8150  cnref1o  10850  1arith  13835  xpsff1o  14347  isffth2  14667  ffthf1o  14670  orbsta  15661  symgextf1o  15704  symgfixf1o  15722  odf1o1  15815  znf1o  17457  cygznlem3  17475  reeff1o  21378  recosf1o  21457  efif1olem4  21467  dvdsmulf1o  22000  eupatrl  22711  unopf1o  24442  nvof1o  25076  ghomf1olem  26453  wwlktovf1o  29435  wlknwwlknbij  29526  wlkiswwlkbij  29533  wwlkextbij0  29545  clwwlkf1o  29641  clwlkf1oclwwlk  29705  frgrancvvdeqlem8  29814  numclwlk1lem2f1o  29870
  Copyright terms: Public domain W3C validator