![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resexg | Structured version Visualization version GIF version |
Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
resexg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resss 5457 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 | |
2 | ssexg 4837 | . 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V) | |
3 | 1, 2 | mpan 706 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 Vcvv 3231 ⊆ wss 3607 ↾ cres 5145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 df-ss 3621 df-res 5155 |
This theorem is referenced by: resex 5478 fvtresfn 6323 offres 7205 ressuppss 7359 ressuppssdif 7361 resixp 7985 fsuppres 8341 climres 14350 setsvalg 15934 setsid 15961 symgfixels 17900 gsumval3lem1 18352 gsumval3lem2 18353 gsum2dlem2 18416 qtopres 21549 tsmspropd 21982 ulmss 24196 vtxdginducedm1 26495 redwlk 26625 hhssva 28242 hhsssm 28243 hhshsslem1 28252 resf1o 29633 eulerpartlemmf 30565 exidres 33807 exidresid 33808 xrnresex 34304 lmhmlnmsplit 37974 pwssplit4 37976 resexd 39635 setsv 41673 |
Copyright terms: Public domain | W3C validator |