Theorem ssv 3939

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

Syntax hints:  Vcvv 3441   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  inv1  4302  unv  4303  vss  4351  pssv  4354  disj2  4365  pwv  4797  unissint  4862  symdifv  4971  trv  5148  intabs  5209  xpss  5535  inxpssres  5536  djussxp  5680  dmv  5756  dmresi  5888  cnvrescnv  6019  rescnvcnv  6028  cocnvcnv1  6077  relrelss  6092  fnresi  6448  dffn2  6489  oprabss  7239  fvresex  7643  ofmres  7667  f1stres  7695  f2ndres  7696  fsplitfpar  7797  domssex2  8661  fineqv  8717  fiint  8779  marypha1lem  8881  marypha2  8887  cantnfval2  9116  inlresf1  9328  inrresf1  9330  djuun  9339  dfac12lem2  9555  dfac12a  9559  fin23lem41  9763  dfacfin7  9810  iunfo  9950  gch2  10086  axpre-sup  10580  wrdv  13872  setscom  16519  isofn  17037  homaf  17282  dmaf  17301  cdaf  17302  prdsinvlem  18200  frgpuplem  18890  gsum2dlem2  19084  gsum2d  19085  mgpf  19305  prdsmgp  19356  prdscrngd  19359  pws1  19362  mulgass3  19383  crngridl  20004  frlmbas  20444  islindf3  20515  ply1lss  20825  coe1fval3  20837  coe1tm  20902  ply1coe  20925  evl1expd  20969  pmatcollpw3lem  21388  clsconn  22035  ptbasfi  22186  upxp  22228  uptx  22230  prdstps  22234  hausdiag  22250  cnmpt1st  22273  cnmpt2nd  22274  fbssint  22443  prdstmdd  22729  prdsxmslem2  23136  isngp2  23203  uniiccdif  24182  wlkdlem1  27472  0vfval  28389  xppreima  30408  2ndimaxp  30409  2ndresdju  30411  xppreima2  30413  1stpreimas  30465  fsuppcurry1  30487  fsuppcurry2  30488  ffsrn  30491  gsummpt2d  30734  gsumpart  30740  lindflbs  30994  elrspunidl  31014  dimval  31089  dimvalfi  31090  qtophaus  31189  cnre2csqlem  31263  cntmeas  31595  eulerpartlemmf  31743  eulerpartlemgf  31747  sseqfv1  31757  sseqfn  31758  sseqfv2  31762  coinflippv  31851  erdszelem2  32552  mpstssv  32899  filnetlem4  33842  bj-0int  34516  bj-idres  34575  elxp8  34788  poimirlem16  35073  poimirlem19  35076  poimirlem20  35077  poimirlem26  35083  poimirlem27  35084  heibor1lem  35247  rmxyelqirr  39851  isnumbasgrplem1  40045  isnumbasgrplem2  40048  dfacbasgrp  40052  resnonrel  40292  comptiunov2i  40407  ntrneiel2  40789  ntrneik4w  40803  conss2  41147