![]() |
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 | ⊢ (A Fn B ↔ (Fun A ∧ dom A = B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | 1, 2 | wfn 4840 | . 2 wff A Fn B |
4 | 1 | wfun 4839 | . . 3 wff Fun A |
5 | 1 | cdm 4288 | . . . 4 class dom A |
6 | 5, 2 | wceq 1242 | . . 3 wff dom A = B |
7 | 4, 6 | wa 97 | . 2 wff (Fun A ∧ dom A = B) |
8 | 3, 7 | wb 98 | 1 wff (A Fn B ↔ (Fun A ∧ dom A = B)) |
Colors of variables: wff set class |
This definition is referenced by: funfn 4874 fnsng 4890 fnprg 4897 fntpg 4898 fntp 4899 fncnv 4908 fneq1 4930 fneq2 4931 nffn 4938 fnfun 4939 fndm 4941 fnun 4948 fnco 4950 fnssresb 4954 fnres 4958 fnresi 4959 fn0 4961 fnopabg 4965 sbcfng 4987 fcoi1 5013 f00 5024 f1cnvcnv 5043 fores 5058 dff1o4 5077 foimacnv 5087 fun11iun 5090 funfvdm 5179 respreima 5238 fpr 5288 fnex 5326 fliftf 5382 fnoprabg 5544 tposfn2 5822 tfrlemibfn 5883 tfri1d 5890 frecuzrdgfn 8879 |
Copyright terms: Public domain | W3C validator |