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

Theorem ssv 3967
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 3489 . 2 (𝑥𝐴𝑥 ∈ V)
21ssriv 3947 1 𝐴 ⊆ V
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3471  wss 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-in 3917  df-ss 3927
This theorem is referenced by:  inv1  4321  unv  4322  vss  4368  pssv  4371  disj2  4380  pwv  4808  unissint  4873  symdifv  4981  trv  5157  intabs  5218  xpss  5544  inxpssres  5545  djussxp  5689  dmv  5765  dmresi  5894  cnvrescnv  6025  rescnvcnv  6034  cocnvcnv1  6083  relrelss  6097  fnresi  6449  dffn2  6489  oprabss  7234  fvresex  7636  ofmres  7660  f1stres  7688  f2ndres  7689  fsplitfpar  7789  domssex2  8653  fineqv  8709  fiint  8771  marypha1lem  8873  marypha2  8879  cantnfval2  9108  inlresf1  9320  inrresf1  9322  djuun  9331  dfac12lem2  9547  dfac12a  9551  fin23lem41  9751  dfacfin7  9798  iunfo  9938  gch2  10074  axpre-sup  10568  wrdv  13860  setscom  16506  isofn  17024  homaf  17269  dmaf  17288  cdaf  17289  prdsinvlem  18187  frgpuplem  18877  gsum2dlem2  19070  gsum2d  19071  mgpf  19288  prdsmgp  19339  prdscrngd  19342  pws1  19345  mulgass3  19366  crngridl  19987  ply1lss  20340  coe1fval3  20352  coe1tm  20417  ply1coe  20440  evl1expd  20484  frlmbas  20875  islindf3  20946  pmatcollpw3lem  21367  clsconn  22014  ptbasfi  22165  upxp  22207  uptx  22209  prdstps  22213  hausdiag  22229  cnmpt1st  22252  cnmpt2nd  22253  fbssint  22422  prdstmdd  22708  prdsxmslem2  23115  isngp2  23182  uniiccdif  24161  wlkdlem1  27451  0vfval  28368  xppreima  30381  xppreima2  30382  1stpreimas  30428  fsuppcurry1  30448  fsuppcurry2  30449  ffsrn  30452  gsummpt2d  30695  lindflbs  30949  dimval  31012  dimvalfi  31013  qtophaus  31111  cnre2csqlem  31161  cntmeas  31493  eulerpartlemmf  31641  eulerpartlemgf  31645  sseqfv1  31655  sseqfn  31656  sseqfv2  31660  coinflippv  31749  erdszelem2  32447  mpstssv  32794  filnetlem4  33737  bj-0int  34411  bj-idres  34470  elxp8  34672  poimirlem16  34955  poimirlem19  34958  poimirlem20  34959  poimirlem26  34965  poimirlem27  34966  heibor1lem  35129  rmxyelqirr  39658  isnumbasgrplem1  39852  isnumbasgrplem2  39855  dfacbasgrp  39859  resnonrel  40099  comptiunov2i  40214  ntrneiel2  40599  ntrneik4w  40613  conss2  40958
  Copyright terms: Public domain W3C validator