Theorem ssv 3962

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.

Step	Hyp	Ref	Expression
1		elex 3459	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3941	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 3438   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922

This theorem is referenced by:  inv1  4351  unv  4352  vss  4399  pssv  4402  disj2  4411  pwv  4858  unissint  4925  symdifv  5038  trv  5215  intabs  5291  xpss  5639  inxpssres  5640  djussxp  5792  dmv  5869  dmresi  6007  cnvrescnv  6148  rescnvcnv  6157  cocnvcnv1  6210  relrelss  6225  fnresi  6615  dffn2  6658  oprabss  7461  fvresex  7902  ofmres  7926  f1stres  7955  f2ndres  7956  fsplitfpar  8058  domssex2  9061  fineqv  9168  fiint  9235  fiintOLD  9236  marypha1lem  9342  marypha2  9348  cantnfval2  9584  cottrcl  9634  inlresf1  9830  inrresf1  9832  djuun  9841  dfac12lem2  10058  dfac12a  10062  fin23lem41  10265  dfacfin7  10312  iunfo  10452  gch2  10588  axpre-sup  11082  wrdv  14454  setscom  17109  isofn  17700  homaf  17955  dmaf  17974  cdaf  17975  prdsinvlem  18946  frgpuplem  19669  gsum2dlem2  19868  gsum2d  19869  prdsmgp  20054  rngmgpf  20060  mgpf  20151  prdscrngd  20225  pws1  20228  mulgass3  20256  crngridl  21205  frlmbas  21680  islindf3  21751  psdmul  22069  ply1lss  22097  coe1fval3  22109  coe1tm  22175  ply1coe  22201  evl1expd  22248  pmatcollpw3lem  22686  clsconn  23333  ptbasfi  23484  upxp  23526  uptx  23528  prdstps  23532  hausdiag  23548  cnmpt1st  23571  cnmpt2nd  23572  fbssint  23741  prdstmdd  24027  prdsxmslem2  24433  isngp2  24501  uniiccdif  25495  wlkdlem1  29644  0vfval  30568  xppreima  32602  2ndimaxp  32603  2ndresdju  32606  xppreima2  32608  1stpreimas  32662  fsuppcurry1  32681  fsuppcurry2  32682  ffsrn  32685  gsummpt2d  33015  gsumpart  33023  elrgspnlem2  33196  lindflbs  33329  elrspunidl  33378  dimval  33575  dimvalfi  33576  qtophaus  33805  cnre2csqlem  33879  cntmeas  34195  eulerpartlemmf  34345  eulerpartlemgf  34349  sseqfv1  34359  sseqfn  34360  sseqfv2  34364  coinflippv  34454  fineqvacALT  35075  gblacfnacd  35077  vonf1owev  35083  wevgblacfn  35084  erdszelem2  35167  mpstssv  35514  filnetlem4  36357  bj-0int  37077  bj-idres  37136  elxp8  37347  poimirlem26  37628  poimirlem27  37629  heibor1lem  37791  isnumbasgrplem1  43077  isnumbasgrplem2  43080  dfacbasgrp  43084  resnonrel  43568  comptiunov2i  43682  ntrneiel2  44062  ntrneik4w  44076  conss2  44419  permaxun  44988  permac8prim  44991  slotresfo  48887  basresposfo  48966  ipoglb0  48982  mreclat  48985  isofnALT  49020  rescofuf  49082  initopropdlem  49229  termopropdlem  49230  zeroopropdlem  49231