ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fo Structured version   GIF version

Definition df-fo 4831
Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fo (𝐹:AontoB ↔ (𝐹 Fn A ran 𝐹 = B))

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class 𝐹
41, 2, 3wfo 4823 . 2 wff 𝐹:AontoB
53, 1wfn 4820 . . 3 wff 𝐹 Fn A
63crn 4269 . . . 4 class ran 𝐹
76, 2wceq 1226 . . 3 wff ran 𝐹 = B
85, 7wa 97 . 2 wff (𝐹 Fn A ran 𝐹 = B)
94, 8wb 98 1 wff (𝐹:AontoB ↔ (𝐹 Fn A ran 𝐹 = B))
Colors of variables: wff set class
This definition is referenced by:  foeq1  5023  foeq2  5024  foeq3  5025  nffo  5026  fof  5027  forn  5030  dffo2  5031  dffn4  5033  fores  5036  dff1o2  5052  dff1o3  5053  foimacnv  5065  foun  5066  fconstfvm  5300  dff1o6  5337  fo1st  5703  fo2nd  5704  tposfo2  5800
  Copyright terms: Public domain W3C validator