Theorem resexg 5442

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

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-res 5126

This theorem is referenced by:  resex  5443  fvtresfn  6284  offres  7163  ressuppss  7314  ressuppssdif  7316  resixp  7943  fsuppres  8300  climres  14306  setsvalg  15887  setsid  15914  symgfixels  17854  gsumval3lem1  18306  gsumval3lem2  18307  gsum2dlem2  18370  qtopres  21501  tsmspropd  21935  ulmss  24151  vtxdginducedm1  26439  redwlk  26569  hhssva  28114  hhsssm  28115  hhshsslem1  28124  resf1o  29505  eulerpartlemmf  30437  exidres  33677  exidresid  33678  lmhmlnmsplit  37657  pwssplit4  37659  resexd  39321  setsv  41348