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

Theorem ssv 3485
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 3091 . 2  |-  ( x  e.  A  ->  x  e.  _V )
21ssriv 3469 1  |-  A  C_  _V
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3082    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-v 3084  df-in 3444  df-ss 3451
This theorem is referenced by:  inv1  3790  unv  3791  vss  3830  pssv  3833  disj2  3841  pwv  4216  unissint  4278  symdifv  4375  trv  4528  intabs  4583  xpss  4958  djussxp  4997  dmv  5067  dmresi  5177  resid  5179  ssrnres  5292  rescnvcnv  5315  cocnvcnv1  5363  relrelss  5376  dffn2  5745  oprabss  6394  fvresex  6778  ofmres  6801  f1stres  6827  f2ndres  6828  domssex2  7736  fineqv  7791  fiint  7852  marypha1lem  7951  marypha2  7957  cantnfval2  8177  oef1o  8206  dfac12lem2  8576  dfac12a  8580  fin23lem41  8784  dfacfin7  8831  iunfo  8966  gch2  9102  axpre-sup  9595  setscom  15146  isofn  15673  homaf  15918  dmaf  15937  cdaf  15938  prdsinvlem  16787  frgpuplem  17415  gsum2dlem2  17596  gsum2d  17597  mgpf  17785  prdsmgp  17831  prdscrngd  17834  pws1  17837  mulgass3  17858  crngridl  18455  ply1lss  18782  coe1fval3  18794  coe1tm  18859  ply1coe  18882  ply1coeOLD  18883  evl1expd  18926  frlmbas  19310  islindf3  19376  pmatcollpw3lem  19799  clscon  20437  ptbasfi  20588  upxp  20630  uptx  20632  prdstps  20636  hausdiag  20652  cnmptid  20668  cnmpt1st  20675  cnmpt2nd  20676  fbssint  20845  prdstmdd  21130  prdsxmslem2  21536  isngp2  21603  uniiccdif  22527  0vfval  26217  xppreima  28244  xppreima2  28245  1stpreimas  28282  ffsrn  28314  gsummpt2d  28545  qtophaus  28665  cnre2csqlem  28718  cntmeas  29050  eulerpartlemmf  29210  eulerpartlemgf  29214  sseqfv1  29224  sseqfn  29225  sseqfv2  29229  coinflippv  29318  erdszelem2  29917  mpstssv  30179  filnetlem4  31036  elxp8  31732  poimirlem16  31914  poimirlem19  31917  poimirlem20  31918  poimirlem26  31924  poimirlem27  31925  heibor1lem  32099  rmxyelqirr  35722  isnumbasgrplem1  35924  isnumbasgrplem2  35927  dfacbasgrp  35931  comptiunov2i  36202  compne  36695  conss2  36698
  Copyright terms: Public domain W3C validator