Theorem ssv 3270

Description: Any class is a subclass of the universal class. Dual of 0ss 3561. (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 2833	. 2 |- ( x e. A -> x e. _V )
2	1	ssriv 3252	1 |- A C_ _V

This proof depends on syntax axioms:   _Vcvv 2821   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  ddifss  3469  inv1  3559  unv  3560  vss  3568  disj2  3580  pwv  3934  trv  4243  xpss  4885  djussxp  4927  dmv  4999  dmresi  5121  resid  5123  ssrnres  5233  rescnvcnv  5253  cocnvcnv1  5301  relrelss  5317  dffn2  5538  oprabss  6177  ofmres  6373  f1stres  6397  f2ndres  6398  fiintim  7244  residfi  7260  djuf1olemr  7400  endjusym  7442  dju1p1e2  7555  suplocexprlemell  8086  seq3val  10917  seqvalcd  10918  seq3-1  10919  seqf  10921  seq3p1  10922  seqf2  10925  seq1cd  10926  seqp1cd  10927  seqclg  10929  seqfeq4g  10988  wrdv  11341  setscom  13449  gzsumwsubmcl  13859  gzsumcl  13862  gsum2dfilem2  14271  prdsinvlem  14302  rngmgpf  14342  mgpf  14421  crngridl  14975  upxp  15515  uptx  15517  cnmptid  15524  cnmpt1st  15531  cnmpt2nd  15532