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 5193 | . 2 |
4 | 1 | wfun 5192 | . . 3 |
5 | 1 | cdm 4611 | . . . 4 |
6 | 5, 2 | wceq 1348 | . . 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 5228 fnsng 5245 fnprg 5253 fntpg 5254 fntp 5255 fncnv 5264 fneq1 5286 fneq2 5287 nffn 5294 fnfun 5295 fndm 5297 fnun 5304 fnco 5306 fnssresb 5310 fnres 5314 fnresi 5315 fn0 5317 fnopabg 5321 sbcfng 5345 fcoi1 5378 f00 5389 f1cnvcnv 5414 fores 5429 dff1o4 5450 foimacnv 5460 fun11iun 5463 funfvdm 5559 respreima 5624 fpr 5678 fnex 5718 fliftf 5778 fnoprabg 5954 tposfn2 6245 tfrlemibfn 6307 tfri1d 6314 tfr1onlembfn 6323 tfri1dALT 6330 tfrcllembfn 6336 sbthlemi9 6942 caseinl 7068 caseinr 7069 ctssdccl 7088 exmidfodomrlemim 7178 axaddf 7830 axmulf 7831 frecuzrdgtcl 10368 frecuzrdgtclt 10377 shftfn 10788 fntopon 12816 |
Copyright terms: Public domain | W3C validator |