![]() |
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 5211 |
. 2
![]() ![]() ![]() ![]() |
4 | 1 | wfun 5210 |
. . 3
![]() ![]() ![]() |
5 | 1 | cdm 4626 |
. . . 4
![]() ![]() ![]() |
6 | 5, 2 | wceq 1353 |
. . 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 5246 fnsng 5263 fnprg 5271 fntpg 5272 fntp 5273 fncnv 5282 fneq1 5304 fneq2 5305 nffn 5312 fnfun 5313 fndm 5315 fnun 5322 fnco 5324 fnssresb 5328 fnres 5332 fnresi 5333 fn0 5335 fnopabg 5339 sbcfng 5363 fcoi1 5396 f00 5407 f1cnvcnv 5432 fores 5447 dff1o4 5469 foimacnv 5479 fun11iun 5482 funfvdm 5579 respreima 5644 fpr 5698 fnex 5738 fliftf 5799 fnoprabg 5975 tposfn2 6266 tfrlemibfn 6328 tfri1d 6335 tfr1onlembfn 6344 tfri1dALT 6351 tfrcllembfn 6357 sbthlemi9 6963 caseinl 7089 caseinr 7090 ctssdccl 7109 exmidfodomrlemim 7199 axaddf 7866 axmulf 7867 frecuzrdgtcl 10411 frecuzrdgtclt 10420 shftfn 10832 imasaddfnlemg 12734 fntopon 13494 |
Copyright terms: Public domain | W3C validator |