Theorem ssv 3955

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

Syntax hints:  Vcvv 3437   ⊆ wss 3898

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915

This theorem is referenced by:  inv1  4347  unv  4348  vss  4395  pssv  4398  disj2  4407  pwv  4857  unissint  4924  symdifv  5038  trv  5215  intabs  5291  xpss  5637  inxpssres  5638  djussxp  5791  dmv  5868  dmresi  6007  cnvrescnv  6149  rescnvcnv  6158  cocnvcnv1  6212  relrelss  6227  fnresi  6617  dffn2  6660  oprabss  7462  fvresex  7900  ofmres  7924  f1stres  7953  f2ndres  7954  fsplitfpar  8056  domssex2  9059  fineqv  9160  fiint  9220  marypha1lem  9326  marypha2  9332  cantnfval2  9568  cottrcl  9618  inlresf1  9817  inrresf1  9819  djuun  9828  dfac12lem2  10045  dfac12a  10049  fin23lem41  10252  dfacfin7  10299  iunfo  10439  gch2  10575  axpre-sup  11069  wrdv  14440  setscom  17095  isofn  17686  homaf  17941  dmaf  17960  cdaf  17961  prdsinvlem  18966  frgpuplem  19688  gsum2dlem2  19887  gsum2d  19888  prdsmgp  20073  rngmgpf  20079  mgpf  20170  prdscrngd  20244  pws1  20247  mulgass3  20275  crngridl  21221  frlmbas  21696  islindf3  21767  psdmul  22084  ply1lss  22112  coe1fval3  22124  coe1tm  22190  ply1coe  22216  evl1expd  22263  pmatcollpw3lem  22701  clsconn  23348  ptbasfi  23499  upxp  23541  uptx  23543  prdstps  23547  hausdiag  23563  cnmpt1st  23586  cnmpt2nd  23587  fbssint  23756  prdstmdd  24042  prdsxmslem2  24447  isngp2  24515  uniiccdif  25509  wlkdlem1  29663  0vfval  30590  xppreima  32631  2ndimaxp  32632  2ndresdju  32635  xppreima2  32637  1stpreimas  32693  fsuppcurry1  32713  fsuppcurry2  32714  ffsrn  32717  gsummpt2d  33038  gsumpart  33046  elrgspnlem2  33219  lindflbs  33353  elrspunidl  33402  dimval  33636  dimvalfi  33637  qtophaus  33872  cnre2csqlem  33946  cntmeas  34262  eulerpartlemmf  34411  eulerpartlemgf  34415  sseqfv1  34425  sseqfn  34426  sseqfv2  34430  coinflippv  34520  fineqvacALT  35163  gblacfnacd  35169  vonf1owev  35175  wevgblacfn  35176  erdszelem2  35259  mpstssv  35606  filnetlem4  36448  bj-0int  37168  bj-idres  37227  elxp8  37438  poimirlem26  37709  poimirlem27  37710  heibor1lem  37872  dmsucmap  38504  isnumbasgrplem1  43221  isnumbasgrplem2  43224  dfacbasgrp  43228  resnonrel  43712  comptiunov2i  43826  ntrneiel2  44206  ntrneik4w  44220  conss2  44562  permaxun  45131  permac8prim  45134  slotresfo  49026  basresposfo  49105  ipoglb0  49121  mreclat  49124  isofnALT  49159  rescofuf  49221  initopropdlem  49368  termopropdlem  49369  zeroopropdlem  49370