Theorem ssv 3164

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 2737	. 2 |- ( x e. A -> x e. _V )
2	1	ssriv 3146	1 |- A C_ _V

Syntax hints:   _Vcvv 2726   C_ wss 3116

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728  df-in 3122  df-ss 3129

This theorem is referenced by:  ddifss  3360  inv1  3445  unv  3446  vss  3456  disj2  3464  pwv  3788  trv  4092  xpss  4712  djussxp  4749  dmv  4820  dmresi  4939  resid  4940  ssrnres  5046  rescnvcnv  5066  cocnvcnv1  5114  relrelss  5130  dffn2  5339  oprabss  5928  ofmres  6104  f1stres  6127  f2ndres  6128  fiintim  6894  djuf1olemr  7019  endjusym  7061  dju1p1e2  7153  suplocexprlemell  7654  seq3val  10393  seqvalcd  10394  seq3-1  10395  seqf  10396  seq3p1  10397  seqf2  10399  seq1cd  10400  seqp1cd  10401  setscom  12434  upxp  12912  uptx  12914  cnmptid  12921  cnmpt1st  12928  cnmpt2nd  12929