![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnresi | Structured version Visualization version GIF version |
Description: Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.) |
Ref | Expression |
---|---|
fnresi | ⊢ ( I ↾ 𝐴) Fn 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funi 6079 | . . 3 ⊢ Fun I | |
2 | funres 6088 | . . 3 ⊢ (Fun I → Fun ( I ↾ 𝐴)) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ Fun ( I ↾ 𝐴) |
4 | dmresi 5613 | . 2 ⊢ dom ( I ↾ 𝐴) = 𝐴 | |
5 | df-fn 6050 | . 2 ⊢ (( I ↾ 𝐴) Fn 𝐴 ↔ (Fun ( I ↾ 𝐴) ∧ dom ( I ↾ 𝐴) = 𝐴)) | |
6 | 3, 4, 5 | mpbir2an 993 | 1 ⊢ ( I ↾ 𝐴) Fn 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1630 I cid 5171 dom cdm 5264 ↾ cres 5266 Fun wfun 6041 Fn wfn 6042 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pr 5053 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ral 3053 df-rex 3054 df-rab 3057 df-v 3340 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-sn 4320 df-pr 4322 df-op 4326 df-br 4803 df-opab 4863 df-id 5172 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-res 5276 df-fun 6049 df-fn 6050 |
This theorem is referenced by: idssxp 6168 f1oi 6333 fninfp 6602 fndifnfp 6604 fnnfpeq0 6606 fveqf1o 6718 weniso 6765 iordsmo 7621 fipreima 8435 dfac9 9148 pmtrfinv 18079 ustuqtop3 22246 fta1blem 24125 qaa 24275 dfiop2 28919 cvmliftlem4 31575 cvmliftlem5 31576 poimirlem15 33735 poimirlem22 33742 ltrnid 35922 rtrclex 38424 dvsid 39030 dflinc2 42707 |
Copyright terms: Public domain | W3C validator |