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

Definition df-f1o 4048
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4695, dff1o3 4696, dff1o4 4698, and dff1o5 4699. 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 4032 . 2
51, 2, 3wf1 4030 . . 3
61, 2, 3wfo 4031 . . 3
75, 6wa 357 . 2
84, 7wb 174 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4684  f1oeq2 4685  f1oeq3 4686  hbf1o 4688  f1of1 4689  dff1o2 4695  dff1o5 4699  f1oco 4713  fo00 4724  dff1o6 4961  fcof1o 4975  f1oweALT 5001  smoiso2 5474  f1finf1o 6095  unfilem2 6121  fofinf1o 6138  alephiso 6540  cnref1o 8385  icoshftf1oii 8608  1arith 10177  orbsta 10954  reeff1o 14031  recosf1o 14096  efif1olem3 14105  unopf1o 15484  dfod2 16047  ghomf1olem 16636  dff1o6f 17764  trnij 18357  soisoi 20239
Copyright terms: Public domain