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

Theorem ssv 3305
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 2901 . 2  |-  ( x  e.  A  ->  x  e.  _V )
21ssriv 3289 1  |-  A  C_  _V
Colors of variables: wff set class
Syntax hints:   _Vcvv 2893    C_ wss 3257
This theorem is referenced by:  inv1  3591  unv  3592  vss  3601  pssv  3604  disj2  3612  pwv  3950  unissint  4010  trv  4249  intabs  4296  xpss  4916  djussxp  4952  dmv  5019  dmresi  5130  resid  5131  ssrnres  5243  rescnvcnv  5266  cocnvcnv1  5314  relrelss  5327  dffn2  5526  fvresex  5915  oprabss  6092  ofmres  6276  f1stres  6301  f2ndres  6302  domssex2  7197  fineqv  7254  fiint  7313  marypha1lem  7367  marypha2  7373  cantnfval2  7551  mapfien  7580  oef1o  7582  dfac12lem2  7951  dfac12a  7955  fin23lem41  8159  dfacfin7  8206  iunfo  8341  gch2  8481  axpre-sup  8971  hashgval2  11573  setscom  13418  homaf  14106  dmaf  14125  cdaf  14126  prdsinvlem  14847  frgpuplem  15325  gsum2d  15467  mgpf  15596  prdsmgp  15637  prdscrngd  15640  pws1  15643  mulgass3  15663  crngridl  16230  ply1lss  16515  coe1fval3  16527  coe1tm  16586  ply1coe  16605  clscon  17408  ptbasfi  17528  upxp  17570  uptx  17572  prdstps  17576  hausdiag  17592  cnmptid  17608  cnmpt1st  17615  cnmpt2nd  17616  fbssint  17785  prdstmdd  18068  prdsxmslem2  18443  isngp2  18509  uniiccdif  19331  evl1expd  19819  0vfval  21927  xppreima  23895  xppreima2  23896  cnre2csqlem  24106  cntmeas  24368  coinflippv  24514  erdszelem2  24651  symdifV  25387  filnetlem4  26095  heibor1lem  26203  rmxyelqirr  26658  frlmbas  26886  isnumbasgrplem1  26929  isnumbasgrplem2  26932  dfacbasgrp  26936  islindf3  26959  compne  27305  conss2  27308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-v 2895  df-in 3264  df-ss 3271
  Copyright terms: Public domain W3C validator