Theorem ssv 3454

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

Syntax hints:   _Vcvv 3047   C_ wss 3406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3049  df-in 3413  df-ss 3420

This theorem is referenced by:  inv1  3763  unv  3764  vss  3803  pssv  3806  disj2  3814  pwv  4200  unissint  4262  symdifv  4359  trv  4512  intabs  4567  xpss  4944  djussxp  4983  dmv  5053  dmresi  5163  resid  5165  ssrnres  5278  rescnvcnv  5301  cocnvcnv1  5349  relrelss  5362  dffn2  5735  oprabss  6387  fvresex  6771  ofmres  6794  f1stres  6820  f2ndres  6821  domssex2  7737  fineqv  7792  fiint  7853  marypha1lem  7952  marypha2  7958  cantnfval2  8179  oef1o  8208  dfac12lem2  8579  dfac12a  8583  fin23lem41  8787  dfacfin7  8834  iunfo  8969  gch2  9105  axpre-sup  9598  setscom  15165  isofn  15692  homaf  15937  dmaf  15956  cdaf  15957  prdsinvlem  16806  frgpuplem  17434  gsum2dlem2  17615  gsum2d  17616  mgpf  17804  prdsmgp  17850  prdscrngd  17853  pws1  17856  mulgass3  17877  crngridl  18474  ply1lss  18801  coe1fval3  18813  coe1tm  18878  ply1coe  18901  ply1coeOLD  18902  evl1expd  18945  frlmbas  19330  islindf3  19396  pmatcollpw3lem  19819  clscon  20457  ptbasfi  20608  upxp  20650  uptx  20652  prdstps  20656  hausdiag  20672  cnmptid  20688  cnmpt1st  20695  cnmpt2nd  20696  fbssint  20865  prdstmdd  21150  prdsxmslem2  21556  isngp2  21623  uniiccdif  22547  0vfval  26237  xppreima  28260  xppreima2  28261  1stpreimas  28298  ffsrn  28326  gsummpt2d  28556  qtophaus  28675  cnre2csqlem  28728  cntmeas  29060  eulerpartlemmf  29220  eulerpartlemgf  29224  sseqfv1  29234  sseqfn  29235  sseqfv2  29239  coinflippv  29328  erdszelem2  29927  mpstssv  30189  filnetlem4  31049  elxp8  31786  poimirlem16  31968  poimirlem19  31971  poimirlem20  31972  poimirlem26  31978  poimirlem27  31979  heibor1lem  32153  rmxyelqirr  35770  isnumbasgrplem1  35972  isnumbasgrplem2  35975  dfacbasgrp  35979  resnonrel  36210  comptiunov2i  36310  compne  36804  conss2  36807