![]() |
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 5230 |
. 2
![]() ![]() ![]() ![]() |
4 | 1 | wfun 5229 |
. . 3
![]() ![]() ![]() |
5 | 1 | cdm 4644 |
. . . 4
![]() ![]() ![]() |
6 | 5, 2 | wceq 1364 |
. . 3
![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: funfn 5265 fnsng 5282 fnprg 5290 fntpg 5291 fntp 5292 fncnv 5301 fneq1 5323 fneq2 5324 nffn 5331 fnfun 5332 fndm 5334 fnun 5341 fnco 5343 fnssresb 5347 fnres 5351 fnresi 5352 fn0 5354 fnopabg 5358 sbcfng 5382 fcoi1 5415 f00 5426 f1cnvcnv 5451 fores 5466 dff1o4 5488 foimacnv 5498 fun11iun 5501 funfvdm 5600 respreima 5665 fpr 5719 fnex 5759 fliftf 5821 fnoprabg 5998 tposfn2 6292 tfrlemibfn 6354 tfri1d 6361 tfr1onlembfn 6370 tfri1dALT 6377 tfrcllembfn 6383 sbthlemi9 6995 caseinl 7121 caseinr 7122 ctssdccl 7141 exmidfodomrlemim 7231 axaddf 7898 axmulf 7899 frecuzrdgtcl 10445 frecuzrdgtclt 10454 shftfn 10868 imasaddfnlemg 12794 fntopon 14001 |
Copyright terms: Public domain | W3C validator |