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

Theorem ssv 3754
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 3340 . 2 (𝑥𝐴𝑥 ∈ V)
21ssriv 3736 1 𝐴 ⊆ V
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3328  wss 3703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-v 3330  df-in 3710  df-ss 3717
This theorem is referenced by:  inv1  4101  unv  4102  vss  4143  pssv  4147  disj2  4156  pwv  4573  unissint  4641  symdifv  4738  trv  4905  intabs  4962  xpss  5270  djussxp  5411  dmv  5484  dmresi  5603  residOLD  5606  ssrnres  5718  rescnvcnv  5743  cocnvcnv1  5795  relrelss  5808  dffn2  6196  oprabss  6899  fvresex  7292  ofmres  7317  f1stres  7345  f2ndres  7346  domssex2  8273  fineqv  8328  fiint  8390  marypha1lem  8492  marypha2  8498  cantnfval2  8727  oef1o  8756  dfac12lem2  9129  dfac12a  9133  fin23lem41  9337  dfacfin7  9384  iunfo  9524  gch2  9660  axpre-sup  10153  wrdv  13477  setscom  16076  isofn  16607  homaf  16852  dmaf  16871  cdaf  16872  prdsinvlem  17696  frgpuplem  18356  gsum2dlem2  18541  gsum2d  18542  mgpf  18730  prdsmgp  18781  prdscrngd  18784  pws1  18787  mulgass3  18808  crngridl  19411  ply1lss  19739  coe1fval3  19751  coe1tm  19816  ply1coe  19839  evl1expd  19882  frlmbas  20272  islindf3  20338  pmatcollpw3lem  20761  clsconn  21406  ptbasfi  21557  upxp  21599  uptx  21601  prdstps  21605  hausdiag  21621  cnmptid  21637  cnmpt1st  21644  cnmpt2nd  21645  fbssint  21814  prdstmdd  22099  prdsxmslem2  22506  isngp2  22573  uniiccdif  23517  wlkdlem1  26760  0vfval  27741  xppreima  29729  xppreima2  29730  1stpreimas  29763  ffsrn  29784  gsummpt2d  30061  qtophaus  30183  cnre2csqlem  30236  cntmeas  30569  eulerpartlemmf  30717  eulerpartlemgf  30721  sseqfv1  30731  sseqfn  30732  sseqfv2  30736  coinflippv  30825  erdszelem2  31452  mpstssv  31714  filnetlem4  32653  bj-0int  33332  elxp8  33501  poimirlem16  33707  poimirlem19  33710  poimirlem20  33711  poimirlem26  33717  poimirlem27  33718  heibor1lem  33890  inxpssres  34369  rmxyelqirr  37946  isnumbasgrplem1  38142  isnumbasgrplem2  38145  dfacbasgrp  38149  resnonrel  38369  comptiunov2i  38469  ntrneiel2  38855  ntrneik4w  38869  compneOLD  39115  conss2  39118
  Copyright terms: Public domain W3C validator