Theorem ssv 3958

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

Syntax hints:  Vcvv 3440   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918

This theorem is referenced by:  inv1  4350  unv  4351  vss  4398  pssv  4401  disj2  4410  pwv  4860  unissint  4927  symdifv  5041  trv  5218  intabs  5294  xpss  5640  inxpssres  5641  djussxp  5794  dmv  5871  dmresi  6011  cnvrescnv  6153  rescnvcnv  6162  cocnvcnv1  6216  relrelss  6231  fnresi  6621  dffn2  6664  oprabss  7466  fvresex  7904  ofmres  7928  f1stres  7957  f2ndres  7958  fsplitfpar  8060  domssex2  9065  fineqv  9167  fiint  9227  marypha1lem  9336  marypha2  9342  cantnfval2  9578  cottrcl  9628  inlresf1  9827  inrresf1  9829  djuun  9838  dfac12lem2  10055  dfac12a  10059  fin23lem41  10262  dfacfin7  10309  iunfo  10449  gch2  10586  axpre-sup  11080  wrdv  14452  setscom  17107  isofn  17699  homaf  17954  dmaf  17973  cdaf  17974  prdsinvlem  18979  frgpuplem  19701  gsum2dlem2  19900  gsum2d  19901  prdsmgp  20086  rngmgpf  20092  mgpf  20183  prdscrngd  20257  pws1  20260  mulgass3  20289  crngridl  21235  frlmbas  21710  islindf3  21781  psdmul  22109  ply1lss  22137  coe1fval3  22149  coe1tm  22215  ply1coe  22242  evl1expd  22289  pmatcollpw3lem  22727  clsconn  23374  ptbasfi  23525  upxp  23567  uptx  23569  prdstps  23573  hausdiag  23589  cnmpt1st  23612  cnmpt2nd  23613  fbssint  23782  prdstmdd  24068  prdsxmslem2  24473  isngp2  24541  uniiccdif  25535  wlkdlem1  29754  0vfval  30681  xppreima  32723  2ndimaxp  32724  2ndresdju  32727  xppreima2  32729  1stpreimas  32785  fsuppcurry1  32803  fsuppcurry2  32804  ffsrn  32807  gsummpt2d  33132  gsumpart  33146  elrgspnlem2  33325  lindflbs  33460  elrspunidl  33509  dimval  33757  dimvalfi  33758  qtophaus  33993  cnre2csqlem  34067  cntmeas  34383  eulerpartlemmf  34532  eulerpartlemgf  34536  sseqfv1  34546  sseqfn  34547  sseqfv2  34551  coinflippv  34641  fineqvacALT  35273  gblacfnacd  35296  vonf1owev  35302  wevgblacfn  35303  erdszelem2  35386  mpstssv  35733  filnetlem4  36575  regsfromunir1  36670  bj-0int  37306  bj-idres  37365  elxp8  37576  poimirlem26  37847  poimirlem27  37848  heibor1lem  38010  dmsucmap  38642  isnumbasgrplem1  43343  isnumbasgrplem2  43346  dfacbasgrp  43350  resnonrel  43833  comptiunov2i  43947  ntrneiel2  44327  ntrneik4w  44341  conss2  44683  permaxun  45252  permac8prim  45255  slotresfo  49144  basresposfo  49223  ipoglb0  49239  mreclat  49242  isofnALT  49276  rescofuf  49338  initopropdlem  49485  termopropdlem  49486  zeroopropdlem  49487