Theorem ssv 3955

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 3935	1 ⊢ 𝐴 ⊆ V

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

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 3916

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  6046  cnvrescnv  6187  rescnvcnv  6198  cocnvcnv1  6252  relrelss  6268  fnresi  6660  dffn2  6703  oprabss  7520  fvresex  7961  ofmres  7985  f1stres  8014  f2ndres  8015  fsplitfpar  8118  domssex2  9140  fineqv  9242  fiint  9302  marypha1lem  9409  marypha2  9415  cantnfval2  9654  cottrcl  9704  inlresf1  9977  inrresf1  9979  djuun  9988  dfac12lem2  10204  dfac12a  10208  fin23lem41  10411  dfacfin7  10458  iunfo  10604  gch2  10741  axpre-sup  11235  wrdv  14654  setscom  17338  isofn  17930  homaf  18185  dmaf  18204  cdaf  18205  prdsinvlem  19239  frgpuplem  19966  gsum2dlem2  20165  gsum2d  20166  prdsmgp  20351  rngmgpf  20359  mgpf  20455  prdscrngd  20531  pws1  20534  mulgass3  20563  crngridl  21555  frlmbas  22041  islindf3  22112  psdmul  22467  ply1lss  22494  coe1fval3  22506  coe1tm  22572  ply1coe  22596  evl1expd  22643  pmatcollpw3lem  23081  clsconn  23728  ptbasfi  23880  upxp  23922  uptx  23924  prdstps  23928  hausdiag  23944  cnmpt1st  23967  cnmpt2nd  23968  fbssint  24137  prdstmdd  24423  prdsxmslem2  24828  isngp2  24896  uniiccdif  25879  wlkdlem1  30243  0vfval  31190  xppreima  33221  2ndimaxp  33222  2ndresdju  33225  xppreima2  33227  1stpreimas  33281  fsuppcurry1  33298  fsuppcurry2  33299  ffsrn  33302  gsummpt2d  33592  gsumpart  33606  elrgspnlem2  33786  lindflbs  33916  elrspunidl  33960  dimval  34215  dimvalfi  34216  qtophaus  34450  cnre2csqlem  34524  cntmeas  34841  eulerpartlemmf  34990  eulerpartlemgf  34994  sseqfv1  35004  sseqfn  35005  sseqfv2  35009  coinflippv  35099  dfscott2  35720  dfscott3  35721  fineqvacALT  35758  gblacfnacd  35854  vonf1wev  35860  vonf1owevOLD  35862  wevgblacfn  35863  wevonprcf1o  35865  vonf1oonf1  35866  erdszelem2  35926  mpstssv  36273  filnetlem4  37139  regsfromunir1  37298  bj-0int  37990  bj-idres  38049  elxp8  38262  poimirlem26  38532  poimirlem27  38533  heibor1lem  38711  dmsucmap  39368  isnumbasgrplem1  44061  isnumbasgrplem2  44064  dfacbasgrp  44068  resnonrel  44551  comptiunov2i  44665  ntrneiel2  45045  ntrneik4w  45059  conss2  45385  permaxun  45953  permac8prim  45956  sqrtnpoly  47887  slotresfo  49951  basresposfo  50030  ipoglb0  50046  mreclat  50049  isofnALT  50083  rescofuf  50145  initopropdlem  50292  termopropdlem  50293  zeroopropdlem  50294