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 5177 | . 2 |
4 | 1 | wfun 5176 | . . 3 |
5 | 1 | cdm 4598 | . . . 4 |
6 | 5, 2 | wceq 1342 | . . 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 5212 fnsng 5229 fnprg 5237 fntpg 5238 fntp 5239 fncnv 5248 fneq1 5270 fneq2 5271 nffn 5278 fnfun 5279 fndm 5281 fnun 5288 fnco 5290 fnssresb 5294 fnres 5298 fnresi 5299 fn0 5301 fnopabg 5305 sbcfng 5329 fcoi1 5362 f00 5373 f1cnvcnv 5398 fores 5413 dff1o4 5434 foimacnv 5444 fun11iun 5447 funfvdm 5543 respreima 5607 fpr 5661 fnex 5701 fliftf 5761 fnoprabg 5934 tposfn2 6225 tfrlemibfn 6287 tfri1d 6294 tfr1onlembfn 6303 tfri1dALT 6310 tfrcllembfn 6316 sbthlemi9 6921 caseinl 7047 caseinr 7048 ctssdccl 7067 exmidfodomrlemim 7148 axaddf 7800 axmulf 7801 frecuzrdgtcl 10337 frecuzrdgtclt 10346 shftfn 10752 fntopon 12569 |
Copyright terms: Public domain | W3C validator |