Theorem ssv 3215

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

Syntax hints:   _Vcvv 2772   C_ wss 3166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  ddifss  3411  inv1  3497  unv  3498  vss  3508  disj2  3516  pwv  3849  trv  4155  xpss  4784  djussxp  4824  dmv  4895  dmresi  5015  resid  5017  ssrnres  5126  rescnvcnv  5146  cocnvcnv1  5194  relrelss  5210  dffn2  5429  oprabss  6033  ofmres  6223  f1stres  6247  f2ndres  6248  fiintim  7030  residfi  7044  djuf1olemr  7158  endjusym  7200  dju1p1e2  7307  suplocexprlemell  7828  seq3val  10607  seqvalcd  10608  seq3-1  10609  seqf  10611  seq3p1  10612  seqf2  10615  seq1cd  10616  seqp1cd  10617  seqclg  10619  seqfeq4g  10678  wrdv  11012  setscom  12905  gsumwsubmcl  13361  gsumfzcl  13364  prdsinvlem  13473  rngmgpf  13732  mgpf  13806  crngridl  14325  upxp  14777  uptx  14779  cnmptid  14786  cnmpt1st  14793  cnmpt2nd  14794