Theorem ssv 3947

Description: Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)

Assertion

Ref	Expression
ssv	⊢ 𝐴 ⊆ V

Proof of Theorem ssv

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3451	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3926	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 3430   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907

This theorem is referenced by:  inv1  4339  unv  4340  vss  4387  pssv  4390  disj2  4399  pwv  4848  unissint  4915  symdifv  5029  trv  5206  intabs  5286  xpss  5640  inxpssres  5641  djussxp  5794  dmv  5871  dmresi  6011  cnvrescnv  6153  rescnvcnv  6162  cocnvcnv1  6216  relrelss  6231  fnresi  6621  dffn2  6664  oprabss  7468  fvresex  7906  ofmres  7930  f1stres  7959  f2ndres  7960  fsplitfpar  8061  domssex2  9068  fineqv  9170  fiint  9230  marypha1lem  9339  marypha2  9345  cantnfval2  9581  cottrcl  9631  inlresf1  9830  inrresf1  9832  djuun  9841  dfac12lem2  10058  dfac12a  10062  fin23lem41  10265  dfacfin7  10312  iunfo  10452  gch2  10589  axpre-sup  11083  wrdv  14482  setscom  17141  isofn  17733  homaf  17988  dmaf  18007  cdaf  18008  prdsinvlem  19016  frgpuplem  19738  gsum2dlem2  19937  gsum2d  19938  prdsmgp  20123  rngmgpf  20129  mgpf  20220  prdscrngd  20292  pws1  20295  mulgass3  20324  crngridl  21270  frlmbas  21745  islindf3  21816  psdmul  22142  ply1lss  22170  coe1fval3  22182  coe1tm  22248  ply1coe  22273  evl1expd  22320  pmatcollpw3lem  22758  clsconn  23405  ptbasfi  23556  upxp  23598  uptx  23600  prdstps  23604  hausdiag  23620  cnmpt1st  23643  cnmpt2nd  23644  fbssint  23813  prdstmdd  24099  prdsxmslem2  24504  isngp2  24572  uniiccdif  25555  wlkdlem1  29764  0vfval  30692  xppreima  32733  2ndimaxp  32734  2ndresdju  32737  xppreima2  32739  1stpreimas  32794  fsuppcurry1  32812  fsuppcurry2  32813  ffsrn  32816  gsummpt2d  33125  gsumpart  33139  elrgspnlem2  33319  lindflbs  33454  elrspunidl  33503  dimval  33760  dimvalfi  33761  qtophaus  33996  cnre2csqlem  34070  cntmeas  34386  eulerpartlemmf  34535  eulerpartlemgf  34539  sseqfv1  34549  sseqfn  34550  sseqfv2  34554  coinflippv  34644  fineqvacALT  35277  gblacfnacd  35300  vonf1owev  35306  wevgblacfn  35307  erdszelem2  35390  mpstssv  35737  filnetlem4  36579  regsfromunir1  36738  bj-0int  37429  bj-idres  37490  elxp8  37701  poimirlem26  37981  poimirlem27  37982  heibor1lem  38144  dmsucmap  38803  isnumbasgrplem1  43547  isnumbasgrplem2  43550  dfacbasgrp  43554  resnonrel  44037  comptiunov2i  44151  ntrneiel2  44531  ntrneik4w  44545  conss2  44887  permaxun  45456  permac8prim  45459  slotresfo  49386  basresposfo  49465  ipoglb0  49481  mreclat  49484  isofnALT  49518  rescofuf  49580  initopropdlem  49727  termopropdlem  49728  zeroopropdlem  49729