HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-f1o 4061
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4721, dff1o3 4722, dff1o4 4724, and dff1o5 4725. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).
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 4045 . 2
51, 2, 3wf1 4043 . . 3
61, 2, 3wfo 4044 . . 3
75, 6wa 357 . 2
84, 7wb 174 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4710  f1oeq2 4711  f1oeq3 4712  hbf1o 4714  f1of1 4715  dff1o2 4721  dff1o5 4725  f1oco 4739  fo00 4750  dff1o6 4991  fcof1o 5005  f1oweALT 5031  smoiso2 5511  f1finf1o 6122  unfilem2 6152  fofinf1o 6169  alephiso 6585  cnref1o 8528  icoshftf1oii 8752  1arith 10328  grpinvf1o 11012  orbsta 11175  reeff1o 14282  recosf1o 14347  efif1olem3 14356  unopf1o 16001  dfod2 16564  ghomf1olem 16952  dff1o6f 18078  trnij 18670  soisoi 20641
Copyright terms: Public domain