![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnssresd | Structured version Visualization version GIF version |
Description: Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
Ref | Expression |
---|---|
fnssresd.1 | ⊢ (𝜑 → 𝐹 Fn 𝐴) |
fnssresd.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
Ref | Expression |
---|---|
fnssresd | ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnssresd.1 | . 2 ⊢ (𝜑 → 𝐹 Fn 𝐴) | |
2 | fnssresd.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | |
3 | fnssres 6663 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) | |
4 | 1, 2, 3 | syl2anc 583 | 1 ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3940 ↾ cres 5668 Fn wfn 6528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-br 5139 df-opab 5201 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-res 5678 df-fun 6535 df-fn 6536 |
This theorem is referenced by: rescnvimafod 7065 fpwwe2lem7 10627 pfxccat1 14648 mdetrsca 22415 2ndresdju 32298 fdifsuppconst 32335 ply1gsumz 33101 dimkerim 33157 rmulccn 33363 subfacp1lem3 34628 satfn 34801 eqresfnbd 41513 tfsconcatrev 42553 ofoafg 42559 xlimconst2 45002 fcoreslem4 46227 |
Copyright terms: Public domain | W3C validator |