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

Theorem ssv 3198
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 2796 . 2  |-  ( x  e.  A  ->  x  e.  _V )
21ssriv 3184 1  |-  A  C_  _V
Colors of variables: wff set class
Syntax hints:   _Vcvv 2788    C_ wss 3152
This theorem is referenced by:  inv1  3481  unv  3482  vss  3491  pssv  3494  disj2  3502  pwv  3826  unissint  3886  trv  4125  intabs  4172  xpss  4793  djussxp  4829  dmv  4894  dmresi  5005  resid  5006  ssrnres  5116  rescnvcnv  5135  cocnvcnv1  5183  relrelss  5196  dffn2  5390  fvresex  5762  oprabss  5933  ofmres  6116  f1stres  6141  f2ndres  6142  domssex2  7021  fineqv  7078  fiint  7133  marypha1lem  7186  marypha2  7192  cantnfval2  7370  mapfien  7399  oef1o  7401  dfac12lem2  7770  dfac12a  7774  fin23lem41  7978  dfacfin7  8025  iunfo  8161  gch2  8301  axpre-sup  8791  hashgval2  11360  incexclem  12295  incexc  12296  setscom  13176  homaf  13862  dmaf  13881  cdaf  13882  prdsinvlem  14603  frgpuplem  15081  gsum2d  15223  mgpf  15352  prdsmgp  15393  prdscrngd  15396  pws1  15399  mulgass3  15419  crngridl  15990  ply1lss  16275  coe1fval3  16289  coe1tm  16349  ply1coe  16368  clscon  17156  ptbasfi  17276  upxp  17317  uptx  17319  prdstps  17323  hausdiag  17339  cnmptid  17355  cnmpt1st  17362  cnmpt2nd  17363  fbssint  17533  prdstmdd  17806  prdsxmslem2  18075  isngp2  18119  uniiccdif  18933  evl1expd  19421  0vfval  21162  ballotlemfmpn  23053  xppreima  23211  xppreima2  23212  df1stres  23243  df2ndres  23244  cnre2csqlem  23294  cntmeas  23553  coinflipspace  23681  coinflippv  23684  erdszelem2  23723  symdifV  24369  vxveqv  25054  residcp  25077  imfstnrelc  25081  rnintintrn  25126  pgapspf  26052  filnetlem4  26330  heibor1lem  26533  rmxyelqirr  26995  frlmbas  27223  isnumbasgrplem1  27266  isnumbasgrplem2  27269  dfacbasgrp  27273  islindf3  27296  compne  27642  conss2  27646
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator