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

Definition df-fo 4823
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 4815 . 2 wff 𝐹:AontoB
53, 1wfn 4812 . . 3 wff 𝐹 Fn A
63crn 4261 . . . 4 class ran 𝐹
76, 2wceq 1223 . . 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  5015  foeq2  5016  foeq3  5017  nffo  5018  fof  5019  forn  5022  dffo2  5023  dffn4  5025  fores  5028  dff1o2  5044  dff1o3  5045  foimacnv  5057  foun  5058  fconstfvm  5292  dff1o6  5329  fo1st  5695  fo2nd  5696  tposfo2  5792
  Copyright terms: Public domain W3C validator