Theorem ssv 3964

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

This proof depends on syntax axioms:  Vcvv 3458   ⊆ wss 3908

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925

This theorem is used by:  inv1  4358  unv  4359  vss  4368  pssv  4372  nvpss  4373  disj2  4421  pwv  4874  unissint  4942  symdifv  5057  trv  5237  intabs  5324  xpss  5682  inxpssres  5683  djussxp  5836  dmv  5917  dmresi  6059  cnvrescnv  6199  rescnvcnv  6210  cocnvcnv1  6264  relrelss  6280  fnresi  6671  dffn2  6714  oprabss  7531  fvresex  7966  ofmres  7990  f1stres  8019  f2ndres  8020  fsplitfpar  8122  domssex2  9135  fineqv  9237  fiint  9296  marypha1lem  9403  marypha2  9409  cantnfval2  9648  cottrcl  9698  inlresf1  9920  inrresf1  9922  djuun  9931  dfac12lem2  10147  dfac12a  10151  fin23lem41  10354  dfacfin7  10401  iunfo  10541  gch2  10678  axpre-sup  11172  wrdv  14586  setscom  17265  isofn  17857  homaf  18112  dmaf  18131  cdaf  18132  prdsinvlem  19146  frgpuplem  19873  gsum2dlem2  20072  gsum2d  20073  prdsmgp  20258  rngmgpf  20266  mgpf  20361  prdscrngd  20436  pws1  20439  mulgass3  20468  crngridl  21456  frlmbas  21942  islindf3  22013  psdmul  22366  ply1lss  22393  coe1fval3  22405  coe1tm  22471  ply1coe  22495  evl1expd  22542  pmatcollpw3lem  22977  clsconn  23624  ptbasfi  23775  upxp  23817  uptx  23819  prdstps  23823  hausdiag  23839  cnmpt1st  23862  cnmpt2nd  23863  fbssint  24032  prdstmdd  24318  prdsxmslem2  24723  isngp2  24791  uniiccdif  25774  wlkdlem1  30067  0vfval  30995  xppreima  33027  2ndimaxp  33028  2ndresdju  33031  xppreima2  33033  1stpreimas  33088  fsuppcurry1  33106  fsuppcurry2  33107  ffsrn  33110  gsummpt2d  33400  gsumpart  33414  elrgspnlem2  33594  lindflbs  33723  elrspunidl  33767  dimval  34022  dimvalfi  34023  qtophaus  34257  cnre2csqlem  34331  cntmeas  34648  eulerpartlemmf  34797  eulerpartlemgf  34801  sseqfv1  34811  sseqfn  34812  sseqfv2  34816  coinflippv  34906  dfscott2  35536  dfscott3  35537  fineqvacALT  35554  gblacfnacd  35610  vonf1wev  35616  vonf1owevOLD  35618  wevgblacfn  35619  wevonprcf1o  35621  vonf1oonf1  35622  erdszelem2  35705  mpstssv  36052  filnetlem4  36933  regsfromunir1  37092  bj-0int  37784  bj-idres  37845  elxp8  38058  poimirlem26  38338  poimirlem27  38339  heibor1lem  38501  dmsucmap  39158  isnumbasgrplem1  43869  isnumbasgrplem2  43872  dfacbasgrp  43876  resnonrel  44359  comptiunov2i  44473  ntrneiel2  44853  ntrneik4w  44867  conss2  45193  permaxun  45761  permac8prim  45764  slotresfo  49718  basresposfo  49797  ipoglb0  49813  mreclat  49816  isofnALT  49850  rescofuf  49912  initopropdlem  50059  termopropdlem  50060  zeroopropdlem  50061