Theorem ssv 3958

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

This proof depends on syntax axioms:  Vcvv 3453   ⊆ wss 3902

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919

This theorem is used by:  inv1  4351  unv  4352  vss  4361  pssv  4365  nvpss  4366  disj2  4414  pwv  4867  unissint  4935  symdifv  5050  trv  5230  intabs  5317  xpss  5675  inxpssres  5676  djussxp  5829  dmv  5910  dmresi  6052  cnvrescnv  6193  rescnvcnv  6204  cocnvcnv1  6258  relrelss  6274  fnresi  6665  dffn2  6708  oprabss  7525  fvresex  7961  ofmres  7985  f1stres  8014  f2ndres  8015  fsplitfpar  8119  domssex2  9139  fineqv  9241  fiint  9300  marypha1lem  9407  marypha2  9413  cantnfval2  9652  cottrcl  9702  inlresf1  9924  inrresf1  9926  djuun  9935  dfac12lem2  10151  dfac12a  10155  fin23lem41  10358  dfacfin7  10405  iunfo  10551  gch2  10688  axpre-sup  11182  wrdv  14598  setscom  17278  isofn  17870  homaf  18125  dmaf  18144  cdaf  18145  prdsinvlem  19178  frgpuplem  19905  gsum2dlem2  20104  gsum2d  20105  prdsmgp  20290  rngmgpf  20298  mgpf  20393  prdscrngd  20468  pws1  20471  mulgass3  20500  crngridl  21488  frlmbas  21974  islindf3  22045  psdmul  22400  ply1lss  22427  coe1fval3  22439  coe1tm  22505  ply1coe  22529  evl1expd  22576  pmatcollpw3lem  23014  clsconn  23661  ptbasfi  23813  upxp  23855  uptx  23857  prdstps  23861  hausdiag  23877  cnmpt1st  23900  cnmpt2nd  23901  fbssint  24070  prdstmdd  24356  prdsxmslem2  24761  isngp2  24829  uniiccdif  25812  wlkdlem1  30148  0vfval  31095  xppreima  33126  2ndimaxp  33127  2ndresdju  33130  xppreima2  33132  1stpreimas  33186  fsuppcurry1  33203  fsuppcurry2  33204  ffsrn  33207  gsummpt2d  33497  gsumpart  33511  elrgspnlem2  33691  lindflbs  33820  elrspunidl  33864  dimval  34119  dimvalfi  34120  qtophaus  34354  cnre2csqlem  34428  cntmeas  34745  eulerpartlemmf  34894  eulerpartlemgf  34898  sseqfv1  34908  sseqfn  34909  sseqfv2  34913  coinflippv  35003  dfscott2  35633  dfscott3  35634  fineqvacALT  35651  gblacfnacd  35707  vonf1wev  35713  vonf1owevOLD  35715  wevgblacfn  35716  wevonprcf1o  35718  vonf1oonf1  35719  erdszelem2  35779  mpstssv  36126  filnetlem4  37008  regsfromunir1  37167  bj-0int  37859  bj-idres  37920  elxp8  38133  poimirlem26  38403  poimirlem27  38404  heibor1lem  38567  dmsucmap  39224  isnumbasgrplem1  43950  isnumbasgrplem2  43953  dfacbasgrp  43957  resnonrel  44440  comptiunov2i  44554  ntrneiel2  44934  ntrneik4w  44948  conss2  45274  permaxun  45842  permac8prim  45845  sqrtnpoly  47769  slotresfo  49833  basresposfo  49912  ipoglb0  49928  mreclat  49931  isofnALT  49965  rescofuf  50027  initopropdlem  50174  termopropdlem  50175  zeroopropdlem  50176