Theorem ssv 3206

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

Syntax hints:   _Vcvv 2763   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  ddifss  3402  inv1  3488  unv  3489  vss  3499  disj2  3507  pwv  3839  trv  4144  xpss  4772  djussxp  4812  dmv  4883  dmresi  5002  resid  5004  ssrnres  5113  rescnvcnv  5133  cocnvcnv1  5181  relrelss  5197  dffn2  5412  oprabss  6012  ofmres  6202  f1stres  6226  f2ndres  6227  fiintim  7001  residfi  7015  djuf1olemr  7129  endjusym  7171  dju1p1e2  7276  suplocexprlemell  7797  seq3val  10569  seqvalcd  10570  seq3-1  10571  seqf  10573  seq3p1  10574  seqf2  10577  seq1cd  10578  seqp1cd  10579  seqclg  10581  seqfeq4g  10640  wrdv  10968  setscom  12743  gsumwsubmcl  13198  gsumfzcl  13201  prdsinvlem  13310  rngmgpf  13569  mgpf  13643  crngridl  14162  upxp  14592  uptx  14594  cnmptid  14601  cnmpt1st  14608  cnmpt2nd  14609