![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-fn | GIF 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 | ⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wfn 5230 | . 2 wff 𝐴 Fn 𝐵 |
4 | 1 | wfun 5229 | . . 3 wff Fun 𝐴 |
5 | 1 | cdm 4644 | . . . 4 class dom 𝐴 |
6 | 5, 2 | wceq 1364 | . . 3 wff dom 𝐴 = 𝐵 |
7 | 4, 6 | wa 104 | . 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵) |
8 | 3, 7 | wb 105 | 1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵)) |
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 5997 tposfn2 6291 tfrlemibfn 6353 tfri1d 6360 tfr1onlembfn 6369 tfri1dALT 6376 tfrcllembfn 6382 sbthlemi9 6994 caseinl 7120 caseinr 7121 ctssdccl 7140 exmidfodomrlemim 7230 axaddf 7897 axmulf 7898 frecuzrdgtcl 10443 frecuzrdgtclt 10452 shftfn 10865 imasaddfnlemg 12791 fntopon 13981 |
Copyright terms: Public domain | W3C validator |