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

Definition df-f1o 4034
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4677, dff1o3 4678, dff1o4 4680, and dff1o5 4681. 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 4018 . 2
51, 2, 3wf1 4016 . . 3
61, 2, 3wfo 4017 . . 3
75, 6wa 357 . 2
84, 7wb 174 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4666  f1oeq2 4667  f1oeq3 4668  hbf1o 4670  f1of1 4671  dff1o2 4677  dff1o5 4681  f1oco 4695  fo00 4706  dff1o6 4943  f1oweALT 4978  smoiso2 5444  f1finf1o 6058  unfilem2 6084  fofinf1o 6101  alephiso 6499  cnref1o 8327  icoshftf1oii 8544  1arith 10078  orbsta 10804  reeff1o 13463  recosf1o 13524  efif1olem3 13531  unopf1o 14792  dfod2 15355  ghomf1olem 15875  dff1o6f 17005  trnij 17613  soisoi 19530
Copyright terms: Public domain