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

Definition df-f1o 4276
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4950, dff1o3 4951, dff1o4 4953, and dff1o5 4954. 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 4260 . 2
51, 2, 3wf1 4258 . . 3
61, 2, 3wfo 4259 . . 3
75, 6wa 357 . 2
84, 7wb 174 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  4939  f1oeq2  4940  f1oeq3  4941  hbf1o  4943  f1of1  4944  dff1o2  4950  dff1o5  4954  f1oco  4968  fo00  4981  dff1o6  5239  fcof1o  5253  soisoi  5266  f1oweALT  5289  smoiso2  5812  f1finf1o  6514  unfilem2  6544  fofinf1o  6562  alephiso  7117  cnref1o  9339  icoshftf1oii  9567  1arith  11172  grpinvf1o  11928  orbsta  12132  dfod2  12174  znf1o  13413  reeff1o  15538  recosf1o  15606  efif1olem4  15615  dvdsmulf1o  16006  unopf1o  17835  ghomf1olem  18705  dff1o6f  19714  trnij  20304
Copyright terms: Public domain