Theorem ssv 3529

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

Syntax hints:   _Vcvv 3118   C_ wss 3481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3120  df-in 3488  df-ss 3495

This theorem is referenced by:  inv1  3817  unv  3818  vss  3868  pssv  3871  disj2  3879  pwv  4250  unissint  4312  trv  4558  intabs  4614  xpss  5115  djussxp  5154  dmv  5224  dmresi  5335  resid  5337  ssrnres  5451  rescnvcnv  5476  cocnvcnv1  5524  relrelss  5537  dffn2  5738  oprabss  6383  fvresex  6768  ofmres  6791  f1stres  6817  f2ndres  6818  domssex2  7689  fineqv  7747  fiint  7809  marypha1lem  7905  marypha2  7911  cantnfval2  8100  cantnfval2OLD  8130  mapfienOLD  8150  oef1o  8153  oef1oOLD  8154  dfac12lem2  8536  dfac12a  8540  fin23lem41  8744  dfacfin7  8791  iunfo  8926  gch2  9065  axpre-sup  9558  hashgval2  12426  setscom  14537  homaf  15232  dmaf  15251  cdaf  15252  prdsinvlem  16050  frgpuplem  16663  gsum2dlem2  16871  gsum2d  16872  gsum2dOLD  16873  mgpf  17082  prdsmgp  17131  prdscrngd  17134  pws1  17137  mulgass3  17158  crngridl  17756  ply1lss  18105  coe1fval3  18117  coe1tm  18184  ply1coe  18207  ply1coeOLD  18208  evl1expd  18251  frlmbas  18655  frlmbasOLD  18656  islindf3  18730  pmatcollpw3lem  19153  clscon  19799  ptbasfi  19950  upxp  19992  uptx  19994  prdstps  19998  hausdiag  20014  cnmptid  20030  cnmpt1st  20037  cnmpt2nd  20038  fbssint  20207  prdstmdd  20490  prdsxmslem2  20900  isngp2  20985  uniiccdif  21855  0vfval  25322  xppreima  27310  xppreima2  27311  ffsrn  27375  qtophaus  27664  cnre2csqlem  27717  cntmeas  28022  eulerpartlemmf  28139  eulerpartlemgf  28143  sseqfv1  28153  sseqfn  28154  sseqfv2  28158  coinflippv  28247  erdszelem2  28461  mpstssv  28724  symdifV  29402  filnetlem4  30126  heibor1lem  30232  rmxyelqirr  30774  isnumbasgrplem1  30978  isnumbasgrplem2  30981  dfacbasgrp  30985  compne  31251  conss2  31254