Theorem ssv 3150

Description: Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)

Assertion

Ref	Expression
ssv	|- A C_ _V

Proof of Theorem ssv

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2723	. 2 |- ( x e. A -> x e. _V )
2	1	ssriv 3132	1 |- A C_ _V

Syntax hints:   _Vcvv 2712   C_ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714  df-in 3108  df-ss 3115

This theorem is referenced by:  ddifss  3345  inv1  3430  unv  3431  vss  3441  disj2  3449  pwv  3772  trv  4075  xpss  4695  djussxp  4732  dmv  4803  dmresi  4922  resid  4923  ssrnres  5029  rescnvcnv  5049  cocnvcnv1  5097  relrelss  5113  dffn2  5322  oprabss  5908  ofmres  6085  f1stres  6108  f2ndres  6109  fiintim  6874  djuf1olemr  6999  endjusym  7041  dju1p1e2  7133  suplocexprlemell  7634  seq3val  10361  seqvalcd  10362  seq3-1  10363  seqf  10364  seq3p1  10365  seqf2  10367  seq1cd  10368  seqp1cd  10369  setscom  12272  upxp  12714  uptx  12716  cnmptid  12723  cnmpt1st  12730  cnmpt2nd  12731