Theorem ssv 3438

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

Syntax hints:   _Vcvv 3031   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033  df-in 3397  df-ss 3404

This theorem is referenced by:  inv1  3764  unv  3765  vss  3805  pssv  3808  disj2  3816  pwv  4189  unissint  4250  symdifv  4347  trv  4502  intabs  4562  xpss  4946  djussxp  4985  dmv  5056  dmresi  5166  resid  5168  ssrnres  5281  rescnvcnv  5305  cocnvcnv1  5353  relrelss  5366  dffn2  5741  oprabss  6401  fvresex  6785  ofmres  6808  f1stres  6834  f2ndres  6835  domssex2  7750  fineqv  7805  fiint  7866  marypha1lem  7965  marypha2  7971  cantnfval2  8192  oef1o  8221  dfac12lem2  8592  dfac12a  8596  fin23lem41  8800  dfacfin7  8847  iunfo  8982  gch2  9118  axpre-sup  9611  wrdv  12733  setscom  15231  isofn  15758  homaf  16003  dmaf  16022  cdaf  16023  prdsinvlem  16872  frgpuplem  17500  gsum2dlem2  17681  gsum2d  17682  mgpf  17870  prdsmgp  17916  prdscrngd  17919  pws1  17922  mulgass3  17943  crngridl  18539  ply1lss  18866  coe1fval3  18878  coe1tm  18943  ply1coe  18966  ply1coeOLD  18967  evl1expd  19010  frlmbas  19395  islindf3  19461  pmatcollpw3lem  19884  clscon  20522  ptbasfi  20673  upxp  20715  uptx  20717  prdstps  20721  hausdiag  20737  cnmptid  20753  cnmpt1st  20760  cnmpt2nd  20761  fbssint  20931  prdstmdd  21216  prdsxmslem2  21622  isngp2  21689  uniiccdif  22614  0vfval  26306  xppreima  28324  xppreima2  28325  1stpreimas  28361  ffsrn  28389  gsummpt2d  28618  qtophaus  28737  cnre2csqlem  28790  cntmeas  29122  eulerpartlemmf  29281  eulerpartlemgf  29285  sseqfv1  29295  sseqfn  29296  sseqfv2  29300  coinflippv  29389  erdszelem2  29987  mpstssv  30249  filnetlem4  31108  elxp8  31844  poimirlem16  32020  poimirlem19  32023  poimirlem20  32024  poimirlem26  32030  poimirlem27  32031  heibor1lem  32205  rmxyelqirr  35829  isnumbasgrplem1  36031  isnumbasgrplem2  36034  dfacbasgrp  36038  resnonrel  36269  comptiunov2i  36369  compne  36863  conss2  36866  1wlkdlem1  39882