Theorem resexg 5898

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 5878	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
2		ssexg 5227	. 2 ⊢ (((𝐴 ↾ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ↾ 𝐵) ∈ V)
3	1, 2	mpan 688	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494   ⊆ wss 3936   ↾ cres 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-res 5567

This theorem is referenced by:  resex  5899  fvtresfn  6770  offres  7684  ressuppss  7849  ressuppssdif  7851  resixp  8497  fsuppres  8858  climres  14932  setsvalg  16512  setsid  16538  symgfixels  18562  gsum2dlem2  19091  qtopres  22306  tsmspropd  22740  ulmss  24985  vtxdginducedm1  27325  redwlk  27454  hhssva  29034  hhsssm  29035  hhshsslem1  29044  resf1o  30466  eulerpartlemmf  31633  exidres  35171  exidresid  35172  xrnresex  35669  unidmqs  35903  lmhmlnmsplit  39707  pwssplit4  39709  resexd  41423  climresdm  42151  setsv  43558