Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fnresi | Structured version Visualization version GIF version |
Description: The restricted identity relation is a function on the restricting class. (Contributed by NM, 27-Aug-2004.) (Proof shortened by BJ, 27-Dec-2023.) |
Ref | Expression |
---|---|
fnresi | ⊢ ( I ↾ 𝐴) Fn 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idfn 6579 | . 2 ⊢ I Fn V | |
2 | ssv 3947 | . 2 ⊢ 𝐴 ⊆ V | |
3 | fnssres 6574 | . 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ ( I ↾ 𝐴) Fn 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3434 ⊆ wss 3889 I cid 5490 ↾ cres 5593 Fn wfn 6442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pr 5355 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2063 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3060 df-rex 3069 df-rab 3224 df-v 3436 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-sn 4565 df-pr 4567 df-op 4571 df-br 5078 df-opab 5140 df-id 5491 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-res 5603 df-fun 6449 df-fn 6450 |
This theorem is referenced by: f1oi 6772 fninfp 7066 fndifnfp 7068 fnnfpeq0 7070 fveqf1o 7195 weniso 7245 iordsmo 8208 fipreima 9153 dfac9 9920 smndex1n0mnd 18579 pmtrfinv 19097 ustuqtop3 23423 fta1blem 25361 qaa 25511 dfiop2 30143 symgcom2 31381 tocycfvres1 31405 tocycfvres2 31406 cvmliftlem4 33278 cvmliftlem5 33279 poimirlem15 35820 poimirlem22 35827 ltrnid 38175 dvsid 41973 dflinc2 45791 |
Copyright terms: Public domain | W3C validator |