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

Theorem ssv 3523
Description: Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
Assertion
Ref Expression
ssv

Proof of Theorem ssv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3118 . 2
21ssriv 3507 1
Colors of variables: wff setvar class
Syntax hints:   cvv 3109  C_wss 3475
This theorem is referenced by:  inv1  3812  unv  3813  vss  3863  pssv  3866  disj2  3874  pwv  4248  unissint  4311  trv  4557  intabs  4613  xpss  5114  djussxp  5153  dmv  5223  dmresi  5334  resid  5336  ssrnres  5450  rescnvcnv  5475  cocnvcnv1  5523  relrelss  5536  dffn2  5737  oprabss  6388  fvresex  6773  ofmres  6796  f1stres  6822  f2ndres  6823  domssex2  7697  fineqv  7755  fiint  7817  marypha1lem  7913  marypha2  7919  cantnfval2  8109  cantnfval2OLD  8139  mapfienOLD  8159  oef1o  8162  oef1oOLD  8163  dfac12lem2  8545  dfac12a  8549  fin23lem41  8753  dfacfin7  8800  iunfo  8935  gch2  9074  axpre-sup  9567  setscom  14662  homaf  15357  dmaf  15376  cdaf  15377  prdsinvlem  16178  frgpuplem  16790  gsum2dlem2  16998  gsum2d  16999  gsum2dOLD  17000  mgpf  17210  prdsmgp  17259  prdscrngd  17262  pws1  17265  mulgass3  17286  crngridl  17886  ply1lss  18235  coe1fval3  18247  coe1tm  18314  ply1coe  18337  ply1coeOLD  18338  evl1expd  18381  frlmbas  18786  frlmbasOLD  18787  islindf3  18861  pmatcollpw3lem  19284  clscon  19931  ptbasfi  20082  upxp  20124  uptx  20126  prdstps  20130  hausdiag  20146  cnmptid  20162  cnmpt1st  20169  cnmpt2nd  20170  fbssint  20339  prdstmdd  20622  prdsxmslem2  21032  isngp2  21117  uniiccdif  21987  0vfval  25499  xppreima  27487  xppreima2  27488  ffsrn  27552  qtophaus  27839  cnre2csqlem  27892  cntmeas  28197  eulerpartlemmf  28314  eulerpartlemgf  28318  sseqfv1  28328  sseqfn  28329  sseqfv2  28333  coinflippv  28422  erdszelem2  28636  mpstssv  28899  symdifV  29475  filnetlem4  30199  heibor1lem  30305  rmxyelqirr  30846  isnumbasgrplem1  31050  isnumbasgrplem2  31053  dfacbasgrp  31057  compne  31349  conss2  31352  isofn  32567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator