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 4897 | . 2 |
4 | 1 | wfun 4896 | . . 3 |
5 | 1 | cdm 4345 | . . . 4 |
6 | 5, 2 | wceq 1243 | . . 3 |
7 | 4, 6 | wa 97 | . 2 |
8 | 3, 7 | wb 98 | 1 |
Colors of variables: wff set class |
This definition is referenced by: funfn 4931 fnsng 4947 fnprg 4954 fntpg 4955 fntp 4956 fncnv 4965 fneq1 4987 fneq2 4988 nffn 4995 fnfun 4996 fndm 4998 fnun 5005 fnco 5007 fnssresb 5011 fnres 5015 fnresi 5016 fn0 5018 fnopabg 5022 sbcfng 5044 fcoi1 5070 f00 5081 f1cnvcnv 5100 fores 5115 dff1o4 5134 foimacnv 5144 fun11iun 5147 funfvdm 5236 respreima 5295 fpr 5345 fnex 5383 fliftf 5439 fnoprabg 5602 tposfn2 5881 tfrlemibfn 5942 tfri1d 5949 frecuzrdgfn 9198 shftfn 9425 |
Copyright terms: Public domain | W3C validator |