![]() |
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 5207 |
. 2
![]() ![]() ![]() ![]() |
4 | 1 | wfun 5206 |
. . 3
![]() ![]() ![]() |
5 | 1 | cdm 4623 |
. . . 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 5242 fnsng 5259 fnprg 5267 fntpg 5268 fntp 5269 fncnv 5278 fneq1 5300 fneq2 5301 nffn 5308 fnfun 5309 fndm 5311 fnun 5318 fnco 5320 fnssresb 5324 fnres 5328 fnresi 5329 fn0 5331 fnopabg 5335 sbcfng 5359 fcoi1 5392 f00 5403 f1cnvcnv 5428 fores 5443 dff1o4 5465 foimacnv 5475 fun11iun 5478 funfvdm 5575 respreima 5640 fpr 5694 fnex 5734 fliftf 5794 fnoprabg 5970 tposfn2 6261 tfrlemibfn 6323 tfri1d 6330 tfr1onlembfn 6339 tfri1dALT 6346 tfrcllembfn 6352 sbthlemi9 6958 caseinl 7084 caseinr 7085 ctssdccl 7104 exmidfodomrlemim 7194 axaddf 7858 axmulf 7859 frecuzrdgtcl 10398 frecuzrdgtclt 10407 shftfn 10817 fntopon 13189 |
Copyright terms: Public domain | W3C validator |