Theorem ssv 3944

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

Syntax hints:  Vcvv 3429   ⊆ wss 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3431  df-in 3893  df-ss 3903

This theorem is referenced by:  inv1  4328  unv  4329  vss  4377  pssv  4380  disj2  4391  pwv  4836  unissint  4903  symdifv  5014  trv  5202  intabs  5264  xpss  5600  inxpssres  5601  djussxp  5747  dmv  5824  dmresi  5954  cnvrescnv  6091  rescnvcnv  6100  cocnvcnv1  6154  relrelss  6169  fnresi  6553  dffn2  6594  oprabss  7371  fvresex  7792  ofmres  7816  f1stres  7844  f2ndres  7845  fsplitfpar  7946  domssex2  8911  fineqv  9025  fiint  9078  marypha1lem  9179  marypha2  9185  cantnfval2  9414  cottrcl  9464  inlresf1  9683  inrresf1  9685  djuun  9694  dfac12lem2  9910  dfac12a  9914  fin23lem41  10118  dfacfin7  10165  iunfo  10305  gch2  10441  axpre-sup  10935  wrdv  14242  setscom  16891  isofn  17497  homaf  17755  dmaf  17774  cdaf  17775  prdsinvlem  18694  frgpuplem  19388  gsum2dlem2  19582  gsum2d  19583  mgpf  19808  prdsmgp  19859  prdscrngd  19862  pws1  19865  mulgass3  19889  crngridl  20519  frlmbas  20972  islindf3  21043  ply1lss  21377  coe1fval3  21389  coe1tm  21454  ply1coe  21477  evl1expd  21521  pmatcollpw3lem  21942  clsconn  22591  ptbasfi  22742  upxp  22784  uptx  22786  prdstps  22790  hausdiag  22806  cnmpt1st  22829  cnmpt2nd  22830  fbssint  22999  prdstmdd  23285  prdsxmslem2  23695  isngp2  23763  uniiccdif  24752  wlkdlem1  28059  0vfval  28976  xppreima  30991  2ndimaxp  30992  2ndresdju  30994  xppreima2  30996  1stpreimas  31046  fsuppcurry1  31068  fsuppcurry2  31069  ffsrn  31072  gsummpt2d  31317  gsumpart  31323  lindflbs  31582  elrspunidl  31614  dimval  31694  dimvalfi  31695  qtophaus  31794  cnre2csqlem  31868  cntmeas  32202  eulerpartlemmf  32350  eulerpartlemgf  32354  sseqfv1  32364  sseqfn  32365  sseqfv2  32369  coinflippv  32458  fineqvacALT  33075  erdszelem2  33162  mpstssv  33509  filnetlem4  34578  bj-0int  35280  bj-idres  35339  elxp8  35550  poimirlem26  35811  poimirlem27  35812  heibor1lem  35975  rmxyelqirr  40740  isnumbasgrplem1  40934  isnumbasgrplem2  40937  dfacbasgrp  40941  resnonrel  41181  comptiunov2i  41295  ntrneiel2  41677  ntrneik4w  41691  conss2  42042  ipoglb0  46258  mreclat  46261