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 6557 | . 2 ⊢ I Fn V | |
2 | ssv 3950 | . 2 ⊢ 𝐴 ⊆ V | |
3 | fnssres 6552 | . 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴) | |
4 | 1, 2, 3 | mp2an 689 | 1 ⊢ ( I ↾ 𝐴) Fn 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3431 ⊆ wss 3892 I cid 5488 ↾ cres 5591 Fn wfn 6426 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-12 2175 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pr 5356 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-ral 3071 df-rex 3072 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-br 5080 df-opab 5142 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-res 5601 df-fun 6433 df-fn 6434 |
This theorem is referenced by: f1oi 6750 fninfp 7041 fndifnfp 7043 fnnfpeq0 7045 fveqf1o 7169 weniso 7219 iordsmo 8177 fipreima 9101 dfac9 9891 smndex1n0mnd 18547 pmtrfinv 19065 ustuqtop3 23391 fta1blem 25329 qaa 25479 dfiop2 30109 symgcom2 31347 tocycfvres1 31371 tocycfvres2 31372 cvmliftlem4 33244 cvmliftlem5 33245 poimirlem15 35786 poimirlem22 35793 ltrnid 38143 dvsid 41917 dflinc2 45718 |
Copyright terms: Public domain | W3C validator |