Theorem ssv 3201

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

Syntax hints:   _Vcvv 2760   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762  df-in 3159  df-ss 3166

This theorem is referenced by:  ddifss  3397  inv1  3483  unv  3484  vss  3494  disj2  3502  pwv  3834  trv  4139  xpss  4767  djussxp  4807  dmv  4878  dmresi  4997  resid  4999  ssrnres  5108  rescnvcnv  5128  cocnvcnv1  5176  relrelss  5192  dffn2  5405  oprabss  6004  ofmres  6188  f1stres  6212  f2ndres  6213  fiintim  6985  residfi  6999  djuf1olemr  7113  endjusym  7155  dju1p1e2  7257  suplocexprlemell  7773  seq3val  10531  seqvalcd  10532  seq3-1  10533  seqf  10535  seq3p1  10536  seqf2  10539  seq1cd  10540  seqp1cd  10541  seqclg  10543  seqfeq4g  10602  wrdv  10930  setscom  12658  gsumwsubmcl  13068  gsumfzcl  13071  rngmgpf  13433  mgpf  13507  crngridl  14026  upxp  14440  uptx  14442  cnmptid  14449  cnmpt1st  14456  cnmpt2nd  14457