Theorem resexg 6027

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-res 5667

This theorem is used by:  resexd  6028  resex  6029  fvtresfn  7016  offres  8016  ressuppss  8225  ressuppssdif  8227  ecelqsw  8814  uniqsw  8820  eceldmqs  8833  resixp  8986  f1imaen3g  9068  dif1enlem  9200  sbthfilem  9238  fsuppres  9409  climres  15768  setsvalg  17370  setsid  17411  symgfixels  19675  qtopres  24044  vtxdginducedm1  30151  redwlk  30278  hhssva  31886  hhsssm  31887  hhshsslem1  31896  resf1o  33389  eulerpartlemmf  35074  exidres  39003  exidresid  39004  xrnresex  39552  unidmqs  39862  disjqmap2  39949  lmhmlnmsplit  44280  climresdm  47063  setsv  48663