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

Definition df-f1o 4022
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4651, dff1o3 4652, dff1o4 4654, and dff1o5 4655. 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 4006 . 2
51, 2, 3wf1 4004 . . 3
61, 2, 3wfo 4005 . . 3
75, 6wa 356 . 2
84, 7wb 173 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4640  f1oeq2 4641  f1oeq3 4642  hbf1o 4644  f1of1 4645  dff1o2 4651  dff1o5 4655  f1oco 4669  fo00 4679  dff1o6 4908  f1oweALT 4943  smoiso2 5400  f1finf1o 6003  unfilem2 6029  fofinf1o 6046  alephiso 6436  cnref1o 8262  icoshftf1oii 8479  1arith 10011  orbsta 10712  reeff1o 13273  recosf1o 13334  efif1olem3 13341  unopf1o 14592  dfod2 15155  ghomf1olem 15523  dff1o6f 16655  trnij 17272  soisoi 18984
Copyright terms: Public domain