Theorem resexg 5897

Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
resexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Proof of Theorem resexg

Step	Hyp	Ref	Expression
1		resss 5877	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
2		ssexg 5226	. 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	mpan 688	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494   ⊆ wss 3935   ↾ cres 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951  df-res 5566

This theorem is referenced by:  resex  5898  fvtresfn  6769  offres  7683  ressuppss  7848  ressuppssdif  7850  resixp  8496  fsuppres  8857  climres  14931  setsvalg  16511  setsid  16537  symgfixels  18561  gsum2dlem2  19090  qtopres  22305  tsmspropd  22739  ulmss  24984  vtxdginducedm1  27324  redwlk  27453  hhssva  29033  hhsssm  29034  hhshsslem1  29043  resf1o  30465  eulerpartlemmf  31633  exidres  35155  exidresid  35156  xrnresex  35653  unidmqs  35887  lmhmlnmsplit  39685  pwssplit4  39687  resexd  41401  climresdm  42129  setsv  43537