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

Definition df-f1o 4199
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4868, dff1o3 4869, dff1o4 4871, and dff1o5 4872. 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 4183 . 2
51, 2, 3wf1 4181 . . 3
61, 2, 3wfo 4182 . . 3
75, 6wa 357 . 2
84, 7wb 174 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4857  f1oeq2 4858  f1oeq3 4859  hbf1o 4861  f1of1 4862  dff1o2 4868  dff1o5 4872  f1oco 4886  fo00 4899  dff1o6 5156  fcof1o 5170  soisoi 5183  f1oweALT 5201  smoiso2 5719  f1finf1o 6384  unfilem2 6414  fofinf1o 6431  alephiso 6958  cnref1o 9179  icoshftf1oii 9404  1arith 10992  grpinvf1o 11740  orbsta 11944  dfod2 11986  znf1o 13166  reeff1o 15265  recosf1o 15333  efif1olem4 15342  unopf1o 17547  ghomf1olem 18399  dff1o6f 19420  trnij 20010
Copyright terms: Public domain