Theorem ssv 3953

Description: Any class is a subclass of the universal class. Dual of 0ss 4350. (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 3472	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3933	1 ⊢ 𝐴 ⊆ V

This proof depends on syntax axioms:  Vcvv 3451   ⊆ wss 3914

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3915

This theorem is used by:  inv1  4348  unv  4349  vss  4358  pssv  4362  nvpss  4363  disj2  4411  pwv  4864  unissint  4932  symdifv  5046  trv  5226  intabs  5310  xpss  5667  inxpssres  5668  djussxp  5823  dmv  5904  dmresi  6044  cnvrescnv  6188  imassrn  6198  rescnvcnv  6206  cocnvcnv1  6260  relrelss  6276  fnresi  6669  dffn2  6712  oprabss  7529  fvresex  7973  ofmres  7997  f1stres  8026  f2ndres  8027  fsplitfpar  8130  domssex2  9157  fineqv  9259  fiint  9319  marypha1lem  9426  marypha2  9432  cantnfval2  9671  cottrcl  9721  inlresf1  9997  inrresf1  9999  djuun  10008  dfac12lem2  10224  dfac12a  10228  fin23lem41  10431  dfacfin7  10478  iunfo  10624  gch2  10761  axpre-sup  11255  wrdv  14675  setscom  17359  isofn  17951  homaf  18206  dmaf  18225  cdaf  18226  prdsinvlem  19260  frgpuplem  19987  gsum2dlem2  20186  gsum2d  20187  prdsmgp  20372  rngmgpf  20380  mgpf  20476  prdscrngd  20552  pws1  20555  mulgass3  20584  crngridl  21576  frlmbas  22062  islindf3  22133  psdmul  22488  ply1lss  22515  coe1fval3  22527  coe1tm  22593  ply1coe  22617  evl1expd  22664  pmatcollpw3lem  23102  clsconn  23749  ptbasfi  23901  upxp  23943  uptx  23945  prdstps  23949  hausdiag  23965  cnmpt1st  23988  cnmpt2nd  23989  fbssint  24158  prdstmdd  24444  prdsxmslem2  24849  isngp2  24917  uniiccdif  25900  wlkdlem1  30262  0vfval  31209  xppreima  33240  2ndimaxp  33241  2ndresdju  33244  xppreima2  33246  1stpreimas  33300  fsuppcurry1  33317  fsuppcurry2  33318  ffsrn  33321  gsummpt2d  33611  gsumpart  33625  elrgspnlem2  33805  lindflbs  33935  elrspunidl  33979  dimval  34234  dimvalfi  34235  qtophaus  34469  cnre2csqlem  34543  cntmeas  34860  eulerpartlemmf  35008  eulerpartlemgf  35012  sseqfv1  35022  sseqfn  35023  sseqfv2  35027  coinflippv  35117  werankwe  35740  dfscott2  35743  dfscott3  35744  acwer1prc  35761  fineqvacALT  35786  gblacfnacd  35882  vonf1wev  35888  vonf1owevOLD  35890  wevgblacfn  35891  wevonprcf1o  35893  vonf1oonf1  35894  vonf1onprcf1ac  35895  erdszelem2  35958  mpstssv  36305  filnetlem4  37170  regsfromunir1  37329  bj-0int  38023  bj-idres  38083  elxp8  38296  poimirlem26  38566  poimirlem27  38567  heibor1lem  38745  dmsucmap  39402  isnumbasgrplem1  44104  isnumbasgrplem2  44107  dfacbasgrp  44111  resnonrel  44593  comptiunov2i  44707  ntrneiel2  45087  ntrneik4w  45101  conss2  45427  permaxun  46002  permac8prim  46005  ishfstruct  46029  sqrtnpoly  47944  slotresfo  50008  basresposfo  50087  ipoglb0  50103  mreclat  50106  isofnALT  50140  rescofuf  50202  initopropdlem  50349  termopropdlem  50350  zeroopropdlem  50351