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

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

Proof of Theorem ssv
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elex 3510 . 2 (𝑥𝐴𝑥 ∈ V)
21ssriv 3968 1 𝐴 ⊆ V
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3492  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-v 3494  df-in 3940  df-ss 3949
This theorem is referenced by:  inv1  4345  unv  4346  vss  4391  pssv  4394  disj2  4403  pwv  4827  unissint  4891  symdifv  4999  trv  5175  intabs  5236  xpss  5564  inxpssres  5565  djussxp  5709  dmv  5785  dmresi  5914  cnvrescnv  6045  rescnvcnv  6054  cocnvcnv1  6103  relrelss  6117  fnresi  6469  dffn2  6509  oprabss  7249  fvresex  7650  ofmres  7674  f1stres  7702  f2ndres  7703  fsplitfpar  7803  domssex2  8665  fineqv  8721  fiint  8783  marypha1lem  8885  marypha2  8891  cantnfval2  9120  inlresf1  9332  inrresf1  9334  djuun  9343  dfac12lem2  9558  dfac12a  9562  fin23lem41  9762  dfacfin7  9809  iunfo  9949  gch2  10085  axpre-sup  10579  wrdv  13865  wrdvOLD  13866  setscom  16515  isofn  17033  homaf  17278  dmaf  17297  cdaf  17298  prdsinvlem  18146  frgpuplem  18827  gsum2dlem2  19020  gsum2d  19021  mgpf  19238  prdsmgp  19289  prdscrngd  19292  pws1  19295  mulgass3  19316  crngridl  19939  ply1lss  20292  coe1fval3  20304  coe1tm  20369  ply1coe  20392  evl1expd  20436  frlmbas  20827  islindf3  20898  pmatcollpw3lem  21319  clsconn  21966  ptbasfi  22117  upxp  22159  uptx  22161  prdstps  22165  hausdiag  22181  cnmpt1st  22204  cnmpt2nd  22205  fbssint  22374  prdstmdd  22659  prdsxmslem2  23066  isngp2  23133  uniiccdif  24106  wlkdlem1  27391  0vfval  28310  xppreima  30322  xppreima2  30323  1stpreimas  30367  fsuppcurry1  30387  fsuppcurry2  30388  ffsrn  30391  gsummpt2d  30614  lindflbs  30867  dimval  30900  dimvalfi  30901  qtophaus  30999  cnre2csqlem  31052  cntmeas  31384  eulerpartlemmf  31532  eulerpartlemgf  31536  sseqfv1  31546  sseqfn  31547  sseqfv2  31551  coinflippv  31640  erdszelem2  32336  mpstssv  32683  filnetlem4  33626  bj-0int  34287  bj-idres  34344  elxp8  34534  poimirlem16  34789  poimirlem19  34792  poimirlem20  34793  poimirlem26  34799  poimirlem27  34800  heibor1lem  34968  rmxyelqirr  39385  isnumbasgrplem1  39579  isnumbasgrplem2  39582  dfacbasgrp  39586  resnonrel  39830  comptiunov2i  39929  ntrneiel2  40314  ntrneik4w  40328  conss2  40652
  Copyright terms: Public domain W3C validator