![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-fn | Unicode version |
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-fn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | wfn 5076 |
. 2
![]() ![]() ![]() ![]() |
4 | 1 | wfun 5075 |
. . 3
![]() ![]() ![]() |
5 | 1 | cdm 4499 |
. . . 4
![]() ![]() ![]() |
6 | 5, 2 | wceq 1314 |
. . 3
![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wa 103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: funfn 5111 fnsng 5128 fnprg 5136 fntpg 5137 fntp 5138 fncnv 5147 fneq1 5169 fneq2 5170 nffn 5177 fnfun 5178 fndm 5180 fnun 5187 fnco 5189 fnssresb 5193 fnres 5197 fnresi 5198 fn0 5200 fnopabg 5204 sbcfng 5228 fcoi1 5261 f00 5272 f1cnvcnv 5297 fores 5312 dff1o4 5331 foimacnv 5341 fun11iun 5344 funfvdm 5438 respreima 5502 fpr 5556 fnex 5596 fliftf 5654 fnoprabg 5826 tposfn2 6117 tfrlemibfn 6179 tfri1d 6186 tfr1onlembfn 6195 tfri1dALT 6202 tfrcllembfn 6208 sbthlemi9 6805 caseinl 6928 caseinr 6929 ctssdccl 6948 exmidfodomrlemim 7005 axaddf 7603 axmulf 7604 frecuzrdgtcl 10078 frecuzrdgtclt 10087 shftfn 10489 fntopon 12034 |
Copyright terms: Public domain | W3C validator |