MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssv Unicode version

Theorem ssv 3360
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.
StepHypRef Expression
1 elex 2956 . 2  |-  ( x  e.  A  ->  x  e.  _V )
21ssriv 3344 1  |-  A  C_  _V
Colors of variables: wff set class
Syntax hints:   _Vcvv 2948    C_ wss 3312
This theorem is referenced by:  inv1  3646  unv  3647  vss  3656  pssv  3659  disj2  3667  pwv  4006  unissint  4066  trv  4306  intabs  4353  xpss  4973  djussxp  5009  dmv  5076  dmresi  5187  resid  5188  ssrnres  5300  rescnvcnv  5323  cocnvcnv1  5371  relrelss  5384  dffn2  5583  fvresex  5973  oprabss  6150  ofmres  6334  f1stres  6359  f2ndres  6360  domssex2  7258  fineqv  7315  fiint  7374  marypha1lem  7429  marypha2  7435  cantnfval2  7613  mapfien  7642  oef1o  7644  dfac12lem2  8013  dfac12a  8017  fin23lem41  8221  dfacfin7  8268  iunfo  8403  gch2  8543  axpre-sup  9033  hashgval2  11640  setscom  13485  homaf  14173  dmaf  14192  cdaf  14193  prdsinvlem  14914  frgpuplem  15392  gsum2d  15534  mgpf  15663  prdsmgp  15704  prdscrngd  15707  pws1  15710  mulgass3  15730  crngridl  16297  ply1lss  16582  coe1fval3  16594  coe1tm  16653  ply1coe  16672  clscon  17481  ptbasfi  17601  upxp  17643  uptx  17645  prdstps  17649  hausdiag  17665  cnmptid  17681  cnmpt1st  17688  cnmpt2nd  17689  fbssint  17858  prdstmdd  18141  prdsxmslem2  18547  isngp2  18632  uniiccdif  19458  evl1expd  19946  0vfval  22073  xppreima  24047  xppreima2  24048  cnre2csqlem  24296  cntmeas  24568  coinflippv  24729  erdszelem2  24866  symdifV  25624  filnetlem4  26347  heibor1lem  26455  rmxyelqirr  26910  frlmbas  27138  isnumbasgrplem1  27181  isnumbasgrplem2  27184  dfacbasgrp  27188  islindf3  27211  compne  27557  conss2  27560
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator