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

Syntax hints:   _Vcvv 2821   C_ wss 3220

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 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 theorem 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 referenced by:  ddifss  3469  inv1  3559  unv  3560  vss  3568  disj2  3580  pwv  3932  trv  4239  xpss  4881  djussxp  4923  dmv  4995  dmresi  5116  resid  5118  ssrnres  5228  rescnvcnv  5248  cocnvcnv1  5296  relrelss  5312  dffn2  5533  oprabss  6167  ofmres  6362  f1stres  6386  f2ndres  6387  fiintim  7231  residfi  7247  djuf1olemr  7387  endjusym  7429  dju1p1e2  7542  suplocexprlemell  8073  seq3val  10878  seqvalcd  10879  seq3-1  10880  seqf  10882  seq3p1  10883  seqf2  10886  seq1cd  10887  seqp1cd  10888  seqclg  10890  seqfeq4g  10949  wrdv  11301  setscom  13373  gzsumwsubmcl  13781  gzsumcl  13784  prdsinvlem  14176  rngmgpf  14214  mgpf  14292  crngridl  14842  upxp  15299  uptx  15301  cnmptid  15308  cnmpt1st  15315  cnmpt2nd  15316