Theorem ssv 3375

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

Syntax hints:   _Vcvv 2971   C_ wss 3327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 2973  df-in 3334  df-ss 3341

This theorem is referenced by:  inv1  3663  unv  3664  vss  3714  pssv  3717  disj2  3725  pwv  4089  unissint  4151  trv  4396  intabs  4452  xpss  4945  djussxp  4984  dmv  5054  dmresi  5160  resid  5162  ssrnres  5275  rescnvcnv  5300  cocnvcnv1  5347  relrelss  5360  dffn2  5559  oprabss  6175  fvresex  6549  ofmres  6572  f1stres  6597  f2ndres  6598  domssex2  7470  fineqv  7527  fiint  7587  marypha1lem  7682  marypha2  7688  cantnfval2  7876  cantnfval2OLD  7906  mapfienOLD  7926  oef1o  7929  oef1oOLD  7930  dfac12lem2  8312  dfac12a  8316  fin23lem41  8520  dfacfin7  8567  iunfo  8702  gch2  8841  axpre-sup  9335  hashgval2  12140  setscom  14203  homaf  14897  dmaf  14916  cdaf  14917  prdsinvlem  15662  frgpuplem  16268  gsum2dlem2  16461  gsum2d  16462  gsum2dOLD  16463  mgpf  16655  prdsmgp  16701  prdscrngd  16704  pws1  16707  mulgass3  16728  crngridl  17319  ply1lss  17651  coe1fval3  17663  coe1tm  17725  ply1coe  17745  ply1coeOLD  17746  evl1expd  17778  frlmbas  18179  frlmbasOLD  18180  islindf3  18254  clscon  19033  ptbasfi  19153  upxp  19195  uptx  19197  prdstps  19201  hausdiag  19217  cnmptid  19233  cnmpt1st  19240  cnmpt2nd  19241  fbssint  19410  prdstmdd  19693  prdsxmslem2  20103  isngp2  20188  uniiccdif  21057  0vfval  23983  xppreima  25963  xppreima2  25964  ffsrn  26028  cnre2csqlem  26339  cntmeas  26639  eulerpartlemmf  26757  eulerpartlemgf  26761  sseqfv1  26771  sseqfn  26772  sseqfv2  26776  coinflippv  26865  erdszelem2  27079  symdifV  27855  filnetlem4  28600  heibor1lem  28706  rmxyelqirr  29249  isnumbasgrplem1  29455  isnumbasgrplem2  29458  dfacbasgrp  29462  compne  29694  conss2  29697