Theorem ssv 3946

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 3450	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3925	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 3429   ⊆ wss 3889

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906

This theorem is referenced by:  inv1  4338  unv  4339  vss  4386  pssv  4389  disj2  4398  pwv  4847  unissint  4914  symdifv  5028  trv  5206  intabs  5290  xpss  5647  inxpssres  5648  djussxp  5800  dmv  5877  dmresi  6017  cnvrescnv  6159  rescnvcnv  6168  cocnvcnv1  6222  relrelss  6237  fnresi  6627  dffn2  6670  oprabss  7475  fvresex  7913  ofmres  7937  f1stres  7966  f2ndres  7967  fsplitfpar  8068  domssex2  9075  fineqv  9177  fiint  9237  marypha1lem  9346  marypha2  9352  cantnfval2  9590  cottrcl  9640  inlresf1  9839  inrresf1  9841  djuun  9850  dfac12lem2  10067  dfac12a  10071  fin23lem41  10274  dfacfin7  10321  iunfo  10461  gch2  10598  axpre-sup  11092  wrdv  14491  setscom  17150  isofn  17742  homaf  17997  dmaf  18016  cdaf  18017  prdsinvlem  19025  frgpuplem  19747  gsum2dlem2  19946  gsum2d  19947  prdsmgp  20132  rngmgpf  20138  mgpf  20229  prdscrngd  20301  pws1  20304  mulgass3  20333  crngridl  21278  frlmbas  21735  islindf3  21806  psdmul  22132  ply1lss  22160  coe1fval3  22172  coe1tm  22238  ply1coe  22263  evl1expd  22310  pmatcollpw3lem  22748  clsconn  23395  ptbasfi  23546  upxp  23588  uptx  23590  prdstps  23594  hausdiag  23610  cnmpt1st  23633  cnmpt2nd  23634  fbssint  23803  prdstmdd  24089  prdsxmslem2  24494  isngp2  24562  uniiccdif  25545  wlkdlem1  29749  0vfval  30677  xppreima  32718  2ndimaxp  32719  2ndresdju  32722  xppreima2  32724  1stpreimas  32779  fsuppcurry1  32797  fsuppcurry2  32798  ffsrn  32801  gsummpt2d  33110  gsumpart  33124  elrgspnlem2  33304  lindflbs  33439  elrspunidl  33488  dimval  33745  dimvalfi  33746  qtophaus  33980  cnre2csqlem  34054  cntmeas  34370  eulerpartlemmf  34519  eulerpartlemgf  34523  sseqfv1  34533  sseqfn  34534  sseqfv2  34538  coinflippv  34628  fineqvacALT  35261  gblacfnacd  35284  vonf1owev  35290  wevgblacfn  35291  erdszelem2  35374  mpstssv  35721  filnetlem4  36563  regsfromunir1  36722  bj-0int  37413  bj-idres  37474  elxp8  37687  poimirlem26  37967  poimirlem27  37968  heibor1lem  38130  dmsucmap  38789  isnumbasgrplem1  43529  isnumbasgrplem2  43532  dfacbasgrp  43536  resnonrel  44019  comptiunov2i  44133  ntrneiel2  44513  ntrneik4w  44527  conss2  44869  permaxun  45438  permac8prim  45441  slotresfo  49374  basresposfo  49453  ipoglb0  49469  mreclat  49472  isofnALT  49506  rescofuf  49568  initopropdlem  49715  termopropdlem  49716  zeroopropdlem  49717