Theorem ssv 3264

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

Syntax hints:   _Vcvv 2815   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817  df-in 3220  df-ss 3227

This theorem is referenced by:  ddifss  3463  inv1  3549  unv  3550  vss  3560  disj2  3568  pwv  3918  trv  4225  xpss  4863  djussxp  4905  dmv  4977  dmresi  5098  resid  5100  ssrnres  5210  rescnvcnv  5230  cocnvcnv1  5278  relrelss  5294  dffn2  5515  oprabss  6147  ofmres  6342  f1stres  6366  f2ndres  6367  fiintim  7204  residfi  7220  djuf1olemr  7358  endjusym  7400  dju1p1e2  7513  suplocexprlemell  8044  seq3val  10846  seqvalcd  10847  seq3-1  10848  seqf  10850  seq3p1  10851  seqf2  10854  seq1cd  10855  seqp1cd  10856  seqclg  10858  seqfeq4g  10917  wrdv  11265  setscom  13336  gsumwsubmcl  13751  gsumfzcl  13754  prdsinvlem  14138  rngmgpf  14176  mgpf  14254  crngridl  14804  upxp  15263  uptx  15265  cnmptid  15272  cnmpt1st  15279  cnmpt2nd  15280