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 5088 | . 2 |
4 | 1 | wfun 5087 | . . 3 |
5 | 1 | cdm 4509 | . . . 4 |
6 | 5, 2 | wceq 1316 | . . 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 5123 fnsng 5140 fnprg 5148 fntpg 5149 fntp 5150 fncnv 5159 fneq1 5181 fneq2 5182 nffn 5189 fnfun 5190 fndm 5192 fnun 5199 fnco 5201 fnssresb 5205 fnres 5209 fnresi 5210 fn0 5212 fnopabg 5216 sbcfng 5240 fcoi1 5273 f00 5284 f1cnvcnv 5309 fores 5324 dff1o4 5343 foimacnv 5353 fun11iun 5356 funfvdm 5452 respreima 5516 fpr 5570 fnex 5610 fliftf 5668 fnoprabg 5840 tposfn2 6131 tfrlemibfn 6193 tfri1d 6200 tfr1onlembfn 6209 tfri1dALT 6216 tfrcllembfn 6222 sbthlemi9 6821 caseinl 6944 caseinr 6945 ctssdccl 6964 exmidfodomrlemim 7025 axaddf 7644 axmulf 7645 frecuzrdgtcl 10140 frecuzrdgtclt 10149 shftfn 10551 fntopon 12102 |
Copyright terms: Public domain | W3C validator |