Theorem ssv 3364

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

Syntax hints:   _Vcvv 2962   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-in 3323  df-ss 3330

This theorem is referenced by:  inv1  3652  unv  3653  vss  3703  pssv  3706  disj2  3714  pwv  4078  unissint  4140  trv  4385  intabs  4441  xpss  4933  djussxp  4972  dmv  5042  dmresi  5149  resid  5151  ssrnres  5264  rescnvcnv  5289  cocnvcnv1  5336  relrelss  5349  dffn2  5548  oprabss  6165  fvresex  6539  ofmres  6562  f1stres  6587  f2ndres  6588  domssex2  7459  fineqv  7516  fiint  7576  marypha1lem  7671  marypha2  7677  cantnfval2  7865  cantnfval2OLD  7895  mapfienOLD  7915  oef1o  7918  oef1oOLD  7919  dfac12lem2  8301  dfac12a  8305  fin23lem41  8509  dfacfin7  8556  iunfo  8691  gch2  8829  axpre-sup  9323  hashgval2  12124  setscom  14186  homaf  14880  dmaf  14899  cdaf  14900  prdsinvlem  15642  frgpuplem  16248  gsum2dlem2  16435  gsum2d  16436  gsum2dOLD  16437  mgpf  16591  prdsmgp  16636  prdscrngd  16639  pws1  16642  mulgass3  16662  crngridl  17241  ply1lss  17550  coe1fval3  17562  coe1tm  17623  ply1coe  17642  frlmbas  18021  frlmbasOLD  18022  islindf3  18096  clscon  18875  ptbasfi  18995  upxp  19037  uptx  19039  prdstps  19043  hausdiag  19059  cnmptid  19075  cnmpt1st  19082  cnmpt2nd  19083  fbssint  19252  prdstmdd  19535  prdsxmslem2  19945  isngp2  20030  uniiccdif  20899  evl1expd  21388  0vfval  23806  xppreima  25787  xppreima2  25788  ffsrn  25853  cnre2csqlem  26193  cntmeas  26493  eulerpartlemmf  26605  eulerpartlemgf  26609  sseqfv1  26619  sseqfn  26620  sseqfv2  26624  coinflippv  26713  erdszelem2  26927  symdifV  27702  filnetlem4  28443  heibor1lem  28549  rmxyelqirr  29093  isnumbasgrplem1  29299  isnumbasgrplem2  29302  dfacbasgrp  29306  compne  29538  conss2  29541