Theorem ssexi 4731

Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)

Hypotheses

Ref	Expression
ssexi.1	⊢ 𝐵 ∈ V
ssexi.2	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
ssexi	⊢ 𝐴 ∈ V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssexi.1	. . 3 ⊢ 𝐵 ∈ V
3	2	ssex 4730	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  zfausab  4738  ord3ex  4782  epse  5021  opabex  6388  fvclex  7031  oprabex  7047  tfrlem16  7376  oev  7481  sbthlem2  7956  phplem2  8025  php  8029  pssnn  8063  dffi3  8220  r0weon  8718  dfac3  8827  dfac5lem4  8832  dfac2  8836  hsmexlem6  9136  domtriomlem  9147  axdc3lem  9155  ac6  9185  brdom7disj  9234  brdom6disj  9235  konigthlem  9269  niex  9582  enqex  9623  npex  9687  enrex  9767  axcnex  9847  reex  9906  nnex  10903  zex  11263  qex  11676  ixxex  12057  ltweuz  12622  prmex  15229  1arithlem1  15465  1arith  15469  prdsval  15938  prdsle  15945  sectfval  16234  sscpwex  16298  issubc  16318  isfunc  16347  fullfunc  16389  fthfunc  16390  isfull  16393  isfth  16397  ipoval  16977  letsr  17050  nmznsg  17461  eqgfval  17465  isghm  17483  symgval  17622  ablfac1b  18292  lpival  19066  ltbval  19292  opsrle  19296  xrsle  19585  xrs10  19604  xrge0cmn  19607  znle  19703  cnmsgngrp  19744  psgninv  19747  cssval  19845  pjfval  19869  istopon  20540  leordtval2  20826  lecldbas  20833  xkoopn  21202  xkouni  21212  xkoccn  21232  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  uzrest  21511  ustfn  21815  ustn0  21834  imasdsf1olem  21988  qtopbaslem  22372  isphtpc  22601  tchex  22824  tchnmfval  22835  bcthlem1  22929  bcthlem5  22933  dyadmbl  23174  itg2seq  23315  lhop1lem  23580  aannenlem3  23889  psercn  23984  abelth  23999  cxpcn2  24287  vmaval  24639  sqff1o  24708  musum  24717  vmadivsum  24971  rpvmasumlem  24976  mudivsum  25019  selberglem1  25034  selberglem2  25035  selberg2lem  25039  selberg2  25040  pntrsumo1  25054  selbergr  25057  iscgrg  25207  isismt  25229  ishlg  25297  ishpg  25451  iscgra  25501  isinag  25529  isleag  25533  sspval  26962  ajfval  27048  shex  27453  chex  27467  hmopex  28118  ressplusf  28981  ressmulgnn  29014  inftmrel  29065  isinftm  29066  dmvlsiga  29519  measbase  29587  ismeas  29589  isrnmeas  29590  faeval  29636  eulerpartlemmf  29764  eulerpartlemgvv  29765  signsplypnf  29953  signsply0  29954  afsval  30002  kur14lem7  30448  kur14lem9  30450  mppsval  30723  dfon2lem7  30938  colinearex  31337  bj-dmtopon  32242  poimirlem4  32583  heibor1lem  32778  rrnval  32796  lsatset  33295  lcvfbr  33325  cmtfvalN  33515  cvrfval  33573  lineset  34042  psubspset  34048  psubclsetN  34240  lautset  34386  pautsetN  34402  tendoset  35065  dicval  35483  eldiophb  36338  pellexlem3  36413  pellexlem5  36415  onfrALTlem3VD  38145  dmvolsal  39240  smfresal  39673  pthsfval  40927  spthsfval  40928  crctS  40994  cyclS  40995  eupths  41367  amgmlemALT  42358