Theorem ssv 3461

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

Syntax hints:   _Vcvv 3058   C_ wss 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-v 3060  df-in 3420  df-ss 3427

This theorem is referenced by:  inv1  3765  unv  3766  vss  3805  pssv  3808  disj2  3816  pwv  4189  unissint  4251  symdifv  4348  trv  4500  intabs  4554  xpss  4929  djussxp  4968  dmv  5038  dmresi  5148  resid  5150  ssrnres  5262  rescnvcnv  5285  cocnvcnv1  5333  relrelss  5346  dffn2  5714  oprabss  6368  fvresex  6756  ofmres  6779  f1stres  6805  f2ndres  6806  domssex2  7714  fineqv  7769  fiint  7830  marypha1lem  7926  marypha2  7932  cantnfval2  8119  cantnfval2OLD  8149  mapfienOLD  8169  oef1o  8172  oef1oOLD  8173  dfac12lem2  8555  dfac12a  8559  fin23lem41  8763  dfacfin7  8810  iunfo  8945  gch2  9082  axpre-sup  9575  setscom  14871  isofn  15386  homaf  15631  dmaf  15650  cdaf  15651  prdsinvlem  16500  frgpuplem  17112  gsum2dlem2  17317  gsum2d  17318  gsum2dOLD  17319  mgpf  17528  prdsmgp  17577  prdscrngd  17580  pws1  17583  mulgass3  17604  crngridl  18204  ply1lss  18553  coe1fval3  18565  coe1tm  18632  ply1coe  18655  ply1coeOLD  18656  evl1expd  18699  frlmbas  19082  frlmbasOLD  19083  islindf3  19151  pmatcollpw3lem  19574  clscon  20221  ptbasfi  20372  upxp  20414  uptx  20416  prdstps  20420  hausdiag  20436  cnmptid  20452  cnmpt1st  20459  cnmpt2nd  20460  fbssint  20629  prdstmdd  20912  prdsxmslem2  21322  isngp2  21407  uniiccdif  22277  0vfval  25899  xppreima  27916  xppreima2  27917  1stpreimas  27954  ffsrn  27985  gsummpt2d  28209  qtophaus  28278  cnre2csqlem  28331  cntmeas  28660  eulerpartlemmf  28806  eulerpartlemgf  28810  sseqfv1  28820  sseqfn  28821  sseqfv2  28825  coinflippv  28914  erdszelem2  29476  mpstssv  29738  filnetlem4  30596  heibor1lem  31567  rmxyelqirr  35187  isnumbasgrplem1  35394  isnumbasgrplem2  35397  dfacbasgrp  35401  comptiunov2i  35665  compne  36177  conss2  36180