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

Definition df-f1o 4014
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4626, dff1o3 4627, dff1o4 4629, and dff1o5 4630. 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 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class F
41, 2, 3wf1o 3998 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 3996 . . 3 wff F:A-1-1->B
61, 2, 3wfo 3997 . . 3 wff F:A-onto->B
75, 6wa 357 . 2 wff (F:A-1-1->B /\ F:A-onto->B)
84, 7wb 174 1 wff (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4615  f1oeq2 4616  f1oeq3 4617  hbf1o 4619  f1of1 4620  dff1o2 4626  dff1o5 4630  f1oco 4644  fo00 4654  dff1o6 4879  f1oweALT 4913  smoiso2 5316  f1finf1o 5909  unfilem2 5934  fofinf1o 5951  alephiso 6337  cnref1o 8138  icoshftf1oii 8355  1arith 9858  reeff1o 12631  recosf1o 12692  efif1olem3 12699  unopf1o 13947  ghomf1olem 14563  dff1o6f 15701  trnij 16308
Copyright terms: Public domain