Theorem ssexi 5028

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 5027	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2166  Vcvv 3414   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803  ax-sep 5005

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812

This theorem is referenced by:  zfausab  5035  ord3ex  5086  epse  5325  opabex  6739  fvclex  7400  oprabex  7416  tfrlem16  7755  oev  7861  sbthlem2  8340  phplem2  8409  php  8413  pssnn  8447  dffi3  8606  r0weon  9148  dfac3  9257  dfac5lem4  9262  dfac2b  9266  dfac2OLD  9268  hsmexlem6  9568  domtriomlem  9579  axdc3lem  9587  ac6  9617  brdom7disj  9668  brdom6disj  9669  konigthlem  9705  niex  10018  enqex  10059  npex  10123  nrex1  10201  enrex  10204  reex  10343  nnex  11357  zex  11713  qex  12083  ixxex  12474  ltweuz  13055  prmex  15763  1arithlem1  15998  1arith  16002  prdsval  16468  prdsle  16475  sectfval  16763  sscpwex  16827  issubc  16847  isfunc  16876  fullfunc  16918  fthfunc  16919  isfull  16922  isfth  16926  ipoval  17507  letsr  17580  nmznsg  17989  eqgfval  17993  isghm  18011  symgval  18149  ablfac1b  18823  lpival  19606  ltbval  19832  opsrle  19836  xrsle  20126  xrs10  20145  xrge0cmn  20148  znle  20244  cnmsgngrp  20284  psgninv  20287  cssval  20389  pjfval  20413  istopon  21087  dmtopon  21098  leordtval2  21387  lecldbas  21394  xkoopn  21763  xkouni  21773  xkoccn  21793  xkoco1cn  21831  xkoco2cn  21832  xkococn  21834  xkoinjcn  21861  uzrest  22071  ustfn  22375  ustn0  22394  imasdsf1olem  22548  qtopbaslem  22932  isphtpc  23163  tcphex  23385  tchnmfval  23396  bcthlem1  23492  bcthlem5  23496  dyadmbl  23766  itg2seq  23908  lhop1lem  24175  aannenlem3  24484  psercn  24579  abelth  24594  cxpcn2  24889  vmaval  25252  sqff1o  25321  musum  25330  vmadivsum  25584  rpvmasumlem  25589  mudivsum  25632  selberglem1  25647  selberglem2  25648  selberg2lem  25652  selberg2  25653  pntrsumo1  25667  selbergr  25670  iscgrg  25824  isismt  25846  ishlg  25914  ishpg  26068  iscgra  26118  isinag  26147  isleag  26151  pthsfval  27023  spthsfval  27024  crcts  27090  cycls  27091  eupths  27576  sspval  28133  ajfval  28219  shex  28624  chex  28638  hmopex  29289  ressplusf  30195  ressmulgnn  30228  inftmrel  30279  isinftm  30280  dmvlsiga  30737  measbase  30805  ismeas  30807  isrnmeas  30808  faeval  30854  eulerpartlemmf  30982  eulerpartlemgvv  30983  signsplypnf  31174  signsply0  31175  afsval  31298  kur14lem7  31740  kur14lem9  31742  mppsval  32015  dfon2lem7  32232  colinearex  32706  cnfinltrel  33786  poimirlem4  33957  heibor1lem  34150  rrnval  34168  lsatset  35065  lcvfbr  35095  cmtfvalN  35285  cvrfval  35343  lineset  35813  psubspset  35819  psubclsetN  36011  lautset  36157  pautsetN  36173  tendoset  36834  dicval  37251  eldiophb  38164  pellexlem3  38239  pellexlem5  38241  onfrALTlem3VD  39941  dmvolsal  41355  smfresal  41789  smfliminflem  41830  amgmlemALT  43445