Theorem resexg 6015

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-res 5662

This theorem is used by:  resexd  6016  resex  6017  fvtresfn  6996  offres  7995  ressuppss  8200  ressuppssdif  8202  ecelqsw  8789  uniqsw  8795  eceldmqs  8808  resixp  8961  f1imaen3g  9043  dif1enlem  9175  sbthfilem  9213  fsuppres  9385  climres  15742  setsvalg  17344  setsid  17385  symgfixels  19648  qtopres  24017  vtxdginducedm1  30124  redwlk  30251  hhssva  31859  hhsssm  31860  hhshsslem1  31869  resf1o  33322  eulerpartlemmf  35007  exidres  38813  exidresid  38814  xrnresex  39362  unidmqs  39672  disjqmap2  39759  lmhmlnmsplit  44089  climresdm  46860  setsv  48460