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

Definition df-f1o 4023
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4639, dff1o3 4640, dff1o4 4642, and dff1o5 4643. 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 4007 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 4005 . . 3 wff F:A-1-1->B
61, 2, 3wfo 4006 . . 3 wff F:A-onto->B
75, 6wa 361 . 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 4628  f1oeq2 4629  f1oeq3 4630  hbf1o 4632  f1of1 4633  dff1o2 4639  dff1o5 4643  f1oco 4657  fo00 4667  dff1o6 4892  f1oweALT 4926  smoiso2 5340  f1finf1o 5933  unfilem2 5958  fofinf1o 5975  alephiso 6360  cnref1o 8161  icoshftf1oii 8378  1arith 9883  reeff1o 12664  recosf1o 12725  efif1olem3 12732  unopf1o 13980  ghomf1olem 14596  dff1o6f 15734  trnij 16341
Copyright terms: Public domain