|   | 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 6018 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 | |
| 2 | ssexg 5322 | . 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V) | |
| 3 | 1, 2 | mpan 690 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3479 ⊆ wss 3950 ↾ cres 5686 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-sep 5295 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-in 3957 df-ss 3967 df-res 5696 | 
| This theorem is referenced by: resexd 6045 resex 6046 fvtresfn 7017 offres 8009 ressuppss 8209 ressuppssdif 8211 resixp 8974 f1imaen3g 9057 dif1enlem 9197 dif1enlemOLD 9198 sbthfilem 9239 fsuppres 9434 climres 15612 setsvalg 17204 setsid 17245 symgfixels 19453 qtopres 23707 vtxdginducedm1 29562 redwlk 29691 hhssva 31277 hhsssm 31278 hhshsslem1 31287 resf1o 32742 eulerpartlemmf 34378 exidres 37886 exidresid 37887 xrnresex 38408 unidmqs 38656 lmhmlnmsplit 43104 climresdm 45870 setsv 47370 | 
| Copyright terms: Public domain | W3C validator |