Theorem ssv 3224

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

Syntax hints:   _Vcvv 2777   C_ wss 3175

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2779  df-in 3181  df-ss 3188

This theorem is referenced by:  ddifss  3420  inv1  3506  unv  3507  vss  3517  disj2  3525  pwv  3864  trv  4171  xpss  4802  djussxp  4842  dmv  4914  dmresi  5034  resid  5036  ssrnres  5145  rescnvcnv  5165  cocnvcnv1  5213  relrelss  5229  dffn2  5448  oprabss  6056  ofmres  6246  f1stres  6270  f2ndres  6271  fiintim  7056  residfi  7070  djuf1olemr  7184  endjusym  7226  dju1p1e2  7338  suplocexprlemell  7863  seq3val  10644  seqvalcd  10645  seq3-1  10646  seqf  10648  seq3p1  10649  seqf2  10652  seq1cd  10653  seqp1cd  10654  seqclg  10656  seqfeq4g  10715  wrdv  11049  setscom  13033  gsumwsubmcl  13489  gsumfzcl  13492  prdsinvlem  13601  rngmgpf  13860  mgpf  13934  crngridl  14453  upxp  14905  uptx  14907  cnmptid  14914  cnmpt1st  14921  cnmpt2nd  14922