Theorem ssv 3328

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

Syntax hints:   _Vcvv 2916   C_ wss 3280

This theorem is referenced by:  inv1  3614  unv  3615  vss  3624  pssv  3627  disj2  3635  pwv  3974  unissint  4034  trv  4274  intabs  4321  xpss  4941  djussxp  4977  dmv  5044  dmresi  5155  resid  5156  ssrnres  5268  rescnvcnv  5291  cocnvcnv1  5339  relrelss  5352  dffn2  5551  fvresex  5941  oprabss  6118  ofmres  6302  f1stres  6327  f2ndres  6328  domssex2  7226  fineqv  7283  fiint  7342  marypha1lem  7396  marypha2  7402  cantnfval2  7580  mapfien  7609  oef1o  7611  dfac12lem2  7980  dfac12a  7984  fin23lem41  8188  dfacfin7  8235  iunfo  8370  gch2  8510  axpre-sup  9000  hashgval2  11607  setscom  13452  homaf  14140  dmaf  14159  cdaf  14160  prdsinvlem  14881  frgpuplem  15359  gsum2d  15501  mgpf  15630  prdsmgp  15671  prdscrngd  15674  pws1  15677  mulgass3  15697  crngridl  16264  ply1lss  16549  coe1fval3  16561  coe1tm  16620  ply1coe  16639  clscon  17446  ptbasfi  17566  upxp  17608  uptx  17610  prdstps  17614  hausdiag  17630  cnmptid  17646  cnmpt1st  17653  cnmpt2nd  17654  fbssint  17823  prdstmdd  18106  prdsxmslem2  18512  isngp2  18597  uniiccdif  19423  evl1expd  19911  0vfval  22038  xppreima  24012  xppreima2  24013  cnre2csqlem  24261  cntmeas  24533  coinflippv  24694  erdszelem2  24831  symdifV  25583  filnetlem4  26300  heibor1lem  26408  rmxyelqirr  26863  frlmbas  27091  isnumbasgrplem1  27134  isnumbasgrplem2  27137  dfacbasgrp  27141  islindf3  27164  compne  27510  conss2  27513

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918  df-in 3287  df-ss 3294