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 4640, dff1o3 4641, dff1o4 4643, and dff1o5 4644. 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 360 . 2
84, 7wb 174 1
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4629  f1oeq2 4630  f1oeq3 4631  hbf1o 4633  f1of1 4634  dff1o2 4640  dff1o5 4644  f1oco 4658  fo00 4668  dff1o6 4896  f1oweALT 4930  smoiso2 5352  f1finf1o 5946  unfilem2 5971  fofinf1o 5988  alephiso 6375  cnref1o 8176  icoshftf1oii 8393  1arith 9903  reeff1o 12932  recosf1o 12993  efif1olem3 13000  unopf1o 14251  ghomf1olem 14991  dff1o6f 16130  trnij 16749  soisoi 18399
Copyright terms: Public domain