Theorem ssv 3946

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

Syntax hints:  Vcvv 3433   ⊆ wss 3888

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  inv1  4329  unv  4330  vss  4378  pssv  4381  disj2  4392  pwv  4837  unissint  4904  symdifv  5016  trv  5204  intabs  5267  xpss  5606  inxpssres  5607  djussxp  5757  dmv  5834  dmresi  5964  cnvrescnv  6103  rescnvcnv  6112  cocnvcnv1  6165  relrelss  6180  fnresi  6570  dffn2  6611  oprabss  7390  fvresex  7811  ofmres  7836  f1stres  7864  f2ndres  7865  fsplitfpar  7968  domssex2  8933  fineqv  9047  fiint  9100  marypha1lem  9201  marypha2  9207  cantnfval2  9436  cottrcl  9486  inlresf1  9682  inrresf1  9684  djuun  9693  dfac12lem2  9909  dfac12a  9913  fin23lem41  10117  dfacfin7  10164  iunfo  10304  gch2  10440  axpre-sup  10934  wrdv  14241  setscom  16890  isofn  17496  homaf  17754  dmaf  17773  cdaf  17774  prdsinvlem  18693  frgpuplem  19387  gsum2dlem2  19581  gsum2d  19582  mgpf  19807  prdsmgp  19858  prdscrngd  19861  pws1  19864  mulgass3  19888  crngridl  20518  frlmbas  20971  islindf3  21042  ply1lss  21376  coe1fval3  21388  coe1tm  21453  ply1coe  21476  evl1expd  21520  pmatcollpw3lem  21941  clsconn  22590  ptbasfi  22741  upxp  22783  uptx  22785  prdstps  22789  hausdiag  22805  cnmpt1st  22828  cnmpt2nd  22829  fbssint  22998  prdstmdd  23284  prdsxmslem2  23694  isngp2  23762  uniiccdif  24751  wlkdlem1  28059  0vfval  28977  xppreima  30992  2ndimaxp  30993  2ndresdju  30995  xppreima2  30997  1stpreimas  31047  fsuppcurry1  31069  fsuppcurry2  31070  ffsrn  31073  gsummpt2d  31318  gsumpart  31324  lindflbs  31583  elrspunidl  31615  dimval  31695  dimvalfi  31696  qtophaus  31795  cnre2csqlem  31869  cntmeas  32203  eulerpartlemmf  32351  eulerpartlemgf  32355  sseqfv1  32365  sseqfn  32366  sseqfv2  32370  coinflippv  32459  fineqvacALT  33076  erdszelem2  33163  mpstssv  33510  filnetlem4  34579  bj-0int  35281  bj-idres  35340  elxp8  35551  poimirlem26  35812  poimirlem27  35813  heibor1lem  35976  rmxyelqirr  40739  isnumbasgrplem1  40933  isnumbasgrplem2  40936  dfacbasgrp  40940  resnonrel  41207  comptiunov2i  41321  ntrneiel2  41703  ntrneik4w  41717  conss2  42068  ipoglb0  46291  mreclat  46294