Theorem ssv 3941

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

Syntax hints:  Vcvv 3422   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  inv1  4325  unv  4326  vss  4374  pssv  4377  disj2  4388  pwv  4833  unissint  4900  symdifv  5011  trv  5199  intabs  5261  xpss  5596  inxpssres  5597  djussxp  5743  dmv  5820  dmresi  5950  cnvrescnv  6087  rescnvcnv  6096  cocnvcnv1  6150  relrelss  6165  fnresi  6545  dffn2  6586  oprabss  7359  fvresex  7776  ofmres  7800  f1stres  7828  f2ndres  7829  fsplitfpar  7930  domssex2  8873  fineqv  8967  fiint  9021  marypha1lem  9122  marypha2  9128  cantnfval2  9357  inlresf1  9604  inrresf1  9606  djuun  9615  dfac12lem2  9831  dfac12a  9835  fin23lem41  10039  dfacfin7  10086  iunfo  10226  gch2  10362  axpre-sup  10856  wrdv  14160  setscom  16809  isofn  17404  homaf  17661  dmaf  17680  cdaf  17681  prdsinvlem  18599  frgpuplem  19293  gsum2dlem2  19487  gsum2d  19488  mgpf  19713  prdsmgp  19764  prdscrngd  19767  pws1  19770  mulgass3  19794  crngridl  20422  frlmbas  20872  islindf3  20943  ply1lss  21277  coe1fval3  21289  coe1tm  21354  ply1coe  21377  evl1expd  21421  pmatcollpw3lem  21840  clsconn  22489  ptbasfi  22640  upxp  22682  uptx  22684  prdstps  22688  hausdiag  22704  cnmpt1st  22727  cnmpt2nd  22728  fbssint  22897  prdstmdd  23183  prdsxmslem2  23591  isngp2  23659  uniiccdif  24647  wlkdlem1  27952  0vfval  28869  xppreima  30884  2ndimaxp  30885  2ndresdju  30887  xppreima2  30889  1stpreimas  30940  fsuppcurry1  30962  fsuppcurry2  30963  ffsrn  30966  gsummpt2d  31211  gsumpart  31217  lindflbs  31476  elrspunidl  31508  dimval  31588  dimvalfi  31589  qtophaus  31688  cnre2csqlem  31762  cntmeas  32094  eulerpartlemmf  32242  eulerpartlemgf  32246  sseqfv1  32256  sseqfn  32257  sseqfv2  32261  coinflippv  32350  fineqvacALT  32967  erdszelem2  33054  mpstssv  33401  cottrcl  33705  filnetlem4  34497  bj-0int  35199  bj-idres  35258  elxp8  35469  poimirlem26  35730  poimirlem27  35731  heibor1lem  35894  rmxyelqirr  40648  isnumbasgrplem1  40842  isnumbasgrplem2  40845  dfacbasgrp  40849  resnonrel  41089  comptiunov2i  41203  ntrneiel2  41585  ntrneik4w  41599  conss2  41950  ipoglb0  46168  mreclat  46171