Theorem ssv 3588

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

Syntax hints:  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

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-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  inv1  3922  unv  3923  vss  3964  pssv  3968  disj2  3976  pwv  4371  unissint  4436  symdifv  4534  trv  4693  intabs  4752  xpss  5149  djussxp  5189  dmv  5262  dmresi  5376  resid  5379  ssrnres  5491  rescnvcnv  5515  cocnvcnv1  5563  relrelss  5576  dffn2  5960  oprabss  6644  fvresex  7032  ofmres  7055  f1stres  7081  f2ndres  7082  domssex2  8005  fineqv  8060  fiint  8122  marypha1lem  8222  marypha2  8228  cantnfval2  8449  oef1o  8478  dfac12lem2  8849  dfac12a  8853  fin23lem41  9057  dfacfin7  9104  iunfo  9240  gch2  9376  axpre-sup  9869  wrdv  13175  setscom  15731  isofn  16258  homaf  16503  dmaf  16522  cdaf  16523  prdsinvlem  17347  frgpuplem  18008  gsum2dlem2  18193  gsum2d  18194  mgpf  18382  prdsmgp  18433  prdscrngd  18436  pws1  18439  mulgass3  18460  crngridl  19059  ply1lss  19387  coe1fval3  19399  coe1tm  19464  ply1coe  19487  evl1expd  19530  frlmbas  19918  islindf3  19984  pmatcollpw3lem  20407  clscon  21043  ptbasfi  21194  upxp  21236  uptx  21238  prdstps  21242  hausdiag  21258  cnmptid  21274  cnmpt1st  21281  cnmpt2nd  21282  fbssint  21452  prdstmdd  21737  prdsxmslem2  22144  isngp2  22211  uniiccdif  23152  0vfval  26845  xppreima  28829  xppreima2  28830  1stpreimas  28866  ffsrn  28892  gsummpt2d  29112  qtophaus  29231  cnre2csqlem  29284  cntmeas  29616  eulerpartlemmf  29764  eulerpartlemgf  29768  sseqfv1  29778  sseqfn  29779  sseqfv2  29783  coinflippv  29872  erdszelem2  30428  mpstssv  30690  filnetlem4  31546  elxp8  32395  poimirlem16  32595  poimirlem19  32598  poimirlem20  32599  poimirlem26  32605  poimirlem27  32606  heibor1lem  32778  rmxyelqirr  36493  isnumbasgrplem1  36690  isnumbasgrplem2  36693  dfacbasgrp  36697  resnonrel  36917  comptiunov2i  37017  ntrneiel2  37404  ntrneik4w  37418  compne  37665  conss2  37668  1wlkdlem1  40891