Theorem resexg 5349

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

Syntax hints:   → wi 4   ∈ wcel 1976  Vcvv 3172   ⊆ wss 3539   ↾ cres 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-res 5040

This theorem is referenced by:  resex  5350  fvtresfn  6178  offres  7031  ressuppss  7178  ressuppssdif  7180  resixp  7806  fsuppres  8160  climres  14100  setsvalg  15665  setsid  15688  symgfixels  17623  gsumval3lem1  18075  gsumval3lem2  18076  gsum2dlem2  18139  qtopres  21253  tsmspropd  21687  ulmss  23872  uhgrares  25603  umgrares  25619  usgrares  25664  usgrares1  25705  cusgrares  25767  redwlk  25902  hhssva  27304  hhsssm  27305  hhshsslem1  27314  resf1o  28699  eulerpartlemmf  29570  exidres  32643  exidresid  32644  lmhmlnmsplit  36471  pwssplit4  36473  red1wlk  40876