Theorem ssv 3223

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

Syntax hints:   _Vcvv 2776   C_ wss 3174

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 2778  df-in 3180  df-ss 3187

This theorem is referenced by:  ddifss  3419  inv1  3505  unv  3506  vss  3516  disj2  3524  pwv  3863  trv  4170  xpss  4801  djussxp  4841  dmv  4913  dmresi  5033  resid  5035  ssrnres  5144  rescnvcnv  5164  cocnvcnv1  5212  relrelss  5228  dffn2  5447  oprabss  6054  ofmres  6244  f1stres  6268  f2ndres  6269  fiintim  7054  residfi  7068  djuf1olemr  7182  endjusym  7224  dju1p1e2  7336  suplocexprlemell  7861  seq3val  10642  seqvalcd  10643  seq3-1  10644  seqf  10646  seq3p1  10647  seqf2  10650  seq1cd  10651  seqp1cd  10652  seqclg  10654  seqfeq4g  10713  wrdv  11047  setscom  12987  gsumwsubmcl  13443  gsumfzcl  13446  prdsinvlem  13555  rngmgpf  13814  mgpf  13888  crngridl  14407  upxp  14859  uptx  14861  cnmptid  14868  cnmpt1st  14875  cnmpt2nd  14876