Theorem ssv 3250

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

Syntax hints:   _Vcvv 2803   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  ddifss  3447  inv1  3533  unv  3534  vss  3544  disj2  3552  pwv  3897  trv  4204  xpss  4840  djussxp  4881  dmv  4953  dmresi  5074  resid  5076  ssrnres  5186  rescnvcnv  5206  cocnvcnv1  5254  relrelss  5270  dffn2  5491  oprabss  6117  ofmres  6307  f1stres  6331  f2ndres  6332  fiintim  7166  residfi  7182  djuf1olemr  7313  endjusym  7355  dju1p1e2  7468  suplocexprlemell  7993  seq3val  10785  seqvalcd  10786  seq3-1  10787  seqf  10789  seq3p1  10790  seqf2  10793  seq1cd  10794  seqp1cd  10795  seqclg  10797  seqfeq4g  10856  wrdv  11195  setscom  13202  gsumwsubmcl  13659  gsumfzcl  13662  prdsinvlem  13771  rngmgpf  14031  mgpf  14105  crngridl  14626  upxp  15083  uptx  15085  cnmptid  15092  cnmpt1st  15099  cnmpt2nd  15100