Theorem ssv 3260

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

Syntax hints:   _Vcvv 2813   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815  df-in 3217  df-ss 3224

This theorem is referenced by:  ddifss  3459  inv1  3545  unv  3546  vss  3556  disj2  3564  pwv  3913  trv  4220  xpss  4858  djussxp  4900  dmv  4972  dmresi  5093  resid  5095  ssrnres  5205  rescnvcnv  5225  cocnvcnv1  5273  relrelss  5289  dffn2  5510  oprabss  6139  ofmres  6329  f1stres  6353  f2ndres  6354  fiintim  7191  residfi  7207  djuf1olemr  7345  endjusym  7387  dju1p1e2  7500  suplocexprlemell  8028  seq3val  10822  seqvalcd  10823  seq3-1  10824  seqf  10826  seq3p1  10827  seqf2  10830  seq1cd  10831  seqp1cd  10832  seqclg  10834  seqfeq4g  10893  wrdv  11240  setscom  13252  gsumwsubmcl  13709  gsumfzcl  13712  prdsinvlem  13821  rngmgpf  14081  mgpf  14155  crngridl  14678  upxp  15137  uptx  15139  cnmptid  15146  cnmpt1st  15153  cnmpt2nd  15154