Theorem ssv 4033

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 3509	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 4012	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 3488   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993

This theorem is referenced by:  inv1  4421  unv  4422  vss  4469  pssv  4472  disj2  4481  pwv  4928  unissint  4996  symdifv  5109  trv  5297  intabs  5367  xpss  5716  inxpssres  5717  djussxp  5870  dmv  5947  dmresi  6081  cnvrescnv  6226  rescnvcnv  6235  cocnvcnv1  6288  relrelss  6304  fnresi  6709  dffn2  6749  oprabss  7557  fvresex  8000  ofmres  8025  f1stres  8054  f2ndres  8055  fsplitfpar  8159  domssex2  9203  fineqv  9326  fiint  9394  fiintOLD  9395  marypha1lem  9502  marypha2  9508  cantnfval2  9738  cottrcl  9788  inlresf1  9984  inrresf1  9986  djuun  9995  dfac12lem2  10214  dfac12a  10218  fin23lem41  10421  dfacfin7  10468  iunfo  10608  gch2  10744  axpre-sup  11238  wrdv  14577  setscom  17227  isofn  17836  homaf  18097  dmaf  18116  cdaf  18117  prdsinvlem  19089  frgpuplem  19814  gsum2dlem2  20013  gsum2d  20014  prdsmgp  20178  rngmgpf  20184  mgpf  20275  prdscrngd  20345  pws1  20348  mulgass3  20379  crngridl  21313  frlmbas  21798  islindf3  21869  psdmul  22193  ply1lss  22219  coe1fval3  22231  coe1tm  22297  ply1coe  22323  evl1expd  22370  pmatcollpw3lem  22810  clsconn  23459  ptbasfi  23610  upxp  23652  uptx  23654  prdstps  23658  hausdiag  23674  cnmpt1st  23697  cnmpt2nd  23698  fbssint  23867  prdstmdd  24153  prdsxmslem2  24563  isngp2  24631  uniiccdif  25632  wlkdlem1  29718  0vfval  30638  xppreima  32664  2ndimaxp  32665  2ndresdju  32667  xppreima2  32669  1stpreimas  32717  fsuppcurry1  32739  fsuppcurry2  32740  ffsrn  32743  gsummpt2d  33032  gsumpart  33038  lindflbs  33372  elrspunidl  33421  dimval  33613  dimvalfi  33614  qtophaus  33782  cnre2csqlem  33856  cntmeas  34190  eulerpartlemmf  34340  eulerpartlemgf  34344  sseqfv1  34354  sseqfn  34355  sseqfv2  34359  coinflippv  34448  fineqvacALT  35074  gblacfnacd  35075  wevgblacfn  35076  erdszelem2  35160  mpstssv  35507  filnetlem4  36347  bj-0int  37067  bj-idres  37126  elxp8  37337  poimirlem26  37606  poimirlem27  37607  heibor1lem  37769  rmxyelqirrOLD  42867  isnumbasgrplem1  43058  isnumbasgrplem2  43061  dfacbasgrp  43065  resnonrel  43554  comptiunov2i  43668  ntrneiel2  44048  ntrneik4w  44062  conss2  44412  ipoglb0  48666  mreclat  48669