Theorem resexg 5998

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-res 5650

This theorem is referenced by:  resexd  5999  resex  6000  fvtresfn  6970  offres  7962  ressuppss  8162  ressuppssdif  8164  ecelqsw  8742  uniqsw  8748  eceldmqs  8760  resixp  8906  f1imaen3g  8987  dif1enlem  9120  dif1enlemOLD  9121  sbthfilem  9162  fsuppres  9344  climres  15541  setsvalg  17136  setsid  17177  symgfixels  19364  qtopres  23585  vtxdginducedm1  29471  redwlk  29600  hhssva  31186  hhsssm  31187  hhshsslem1  31196  resf1o  32653  eulerpartlemmf  34366  exidres  37872  exidresid  37873  xrnresex  38392  unidmqs  38646  lmhmlnmsplit  43076  climresdm  45848  setsv  47379