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

Theorem ssv 3211
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 2809 . 2  |-  ( x  e.  A  ->  x  e.  _V )
21ssriv 3197 1  |-  A  C_  _V
Colors of variables: wff set class
Syntax hints:   _Vcvv 2801    C_ wss 3165
This theorem is referenced by:  inv1  3494  unv  3495  vss  3504  pssv  3507  disj2  3515  pwv  3842  unissint  3902  trv  4141  intabs  4188  xpss  4809  djussxp  4845  dmv  4910  dmresi  5021  resid  5022  ssrnres  5132  rescnvcnv  5151  cocnvcnv1  5199  relrelss  5212  dffn2  5406  fvresex  5778  oprabss  5949  ofmres  6132  f1stres  6157  f2ndres  6158  domssex2  7037  fineqv  7094  fiint  7149  marypha1lem  7202  marypha2  7208  cantnfval2  7386  mapfien  7415  oef1o  7417  dfac12lem2  7786  dfac12a  7790  fin23lem41  7994  dfacfin7  8041  iunfo  8177  gch2  8317  axpre-sup  8807  hashgval2  11376  incexclem  12311  incexc  12312  setscom  13192  homaf  13878  dmaf  13897  cdaf  13898  prdsinvlem  14619  frgpuplem  15097  gsum2d  15239  mgpf  15368  prdsmgp  15409  prdscrngd  15412  pws1  15415  mulgass3  15435  crngridl  16006  ply1lss  16291  coe1fval3  16305  coe1tm  16365  ply1coe  16384  clscon  17172  ptbasfi  17292  upxp  17333  uptx  17335  prdstps  17339  hausdiag  17355  cnmptid  17371  cnmpt1st  17378  cnmpt2nd  17379  fbssint  17549  prdstmdd  17822  prdsxmslem2  18091  isngp2  18135  uniiccdif  18949  evl1expd  19437  0vfval  21178  ballotlemfmpn  23069  xppreima  23226  xppreima2  23227  df1stres  23258  df2ndres  23259  cnre2csqlem  23309  cntmeas  23568  coinflipspace  23696  coinflippv  23699  erdszelem2  23738  symdifV  24440  vxveqv  25157  residcp  25180  imfstnrelc  25184  rnintintrn  25229  pgapspf  26155  filnetlem4  26433  heibor1lem  26636  rmxyelqirr  27098  frlmbas  27326  isnumbasgrplem1  27369  isnumbasgrplem2  27372  dfacbasgrp  27376  islindf3  27399  compne  27745  conss2  27749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator