Theorem ssv 3215

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

Syntax hints:   _Vcvv 2772   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  ddifss  3411  inv1  3497  unv  3498  vss  3508  disj2  3516  pwv  3849  trv  4154  xpss  4783  djussxp  4823  dmv  4894  dmresi  5014  resid  5016  ssrnres  5125  rescnvcnv  5145  cocnvcnv1  5193  relrelss  5209  dffn2  5427  oprabss  6031  ofmres  6221  f1stres  6245  f2ndres  6246  fiintim  7028  residfi  7042  djuf1olemr  7156  endjusym  7198  dju1p1e2  7305  suplocexprlemell  7826  seq3val  10605  seqvalcd  10606  seq3-1  10607  seqf  10609  seq3p1  10610  seqf2  10613  seq1cd  10614  seqp1cd  10615  seqclg  10617  seqfeq4g  10676  wrdv  11010  setscom  12872  gsumwsubmcl  13328  gsumfzcl  13331  prdsinvlem  13440  rngmgpf  13699  mgpf  13773  crngridl  14292  upxp  14744  uptx  14746  cnmptid  14753  cnmpt1st  14760  cnmpt2nd  14761