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

Theorem ssv 3370
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 2966 . 2  |-  ( x  e.  A  ->  x  e.  _V )
21ssriv 3354 1  |-  A  C_  _V
Colors of variables: wff set class
Syntax hints:   _Vcvv 2958    C_ wss 3322
This theorem is referenced by:  inv1  3656  unv  3657  vss  3666  pssv  3669  disj2  3677  pwv  4016  unissint  4076  trv  4317  intabs  4364  xpss  4985  djussxp  5021  dmv  5088  dmresi  5199  resid  5200  ssrnres  5312  rescnvcnv  5335  cocnvcnv1  5383  relrelss  5396  dffn2  5595  fvresex  5985  oprabss  6162  ofmres  6346  f1stres  6371  f2ndres  6372  domssex2  7270  fineqv  7327  fiint  7386  marypha1lem  7441  marypha2  7447  cantnfval2  7627  mapfien  7656  oef1o  7658  dfac12lem2  8029  dfac12a  8033  fin23lem41  8237  dfacfin7  8284  iunfo  8419  gch2  8555  axpre-sup  9049  hashgval2  11657  setscom  13502  homaf  14190  dmaf  14209  cdaf  14210  prdsinvlem  14931  frgpuplem  15409  gsum2d  15551  mgpf  15680  prdsmgp  15721  prdscrngd  15724  pws1  15727  mulgass3  15747  crngridl  16314  ply1lss  16599  coe1fval3  16611  coe1tm  16670  ply1coe  16689  clscon  17498  ptbasfi  17618  upxp  17660  uptx  17662  prdstps  17666  hausdiag  17682  cnmptid  17698  cnmpt1st  17705  cnmpt2nd  17706  fbssint  17875  prdstmdd  18158  prdsxmslem2  18564  isngp2  18649  uniiccdif  19475  evl1expd  19963  0vfval  22090  xppreima  24064  xppreima2  24065  cnre2csqlem  24313  cntmeas  24585  coinflippv  24746  erdszelem2  24883  symdifV  25675  filnetlem4  26424  heibor1lem  26532  rmxyelqirr  26987  frlmbas  27214  isnumbasgrplem1  27257  isnumbasgrplem2  27260  dfacbasgrp  27264  islindf3  27287  compne  27633  conss2  27636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator