Theorem ssv 3959

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

Syntax hints:  Vcvv 3436   ⊆ wss 3902

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919

This theorem is referenced by:  inv1  4348  unv  4349  vss  4396  pssv  4399  disj2  4408  pwv  4856  unissint  4922  symdifv  5034  trv  5211  intabs  5287  xpss  5632  inxpssres  5633  djussxp  5785  dmv  5862  dmresi  6001  cnvrescnv  6142  rescnvcnv  6151  cocnvcnv1  6205  relrelss  6220  fnresi  6610  dffn2  6653  oprabss  7454  fvresex  7892  ofmres  7916  f1stres  7945  f2ndres  7946  fsplitfpar  8048  domssex2  9050  fineqv  9151  fiint  9211  marypha1lem  9317  marypha2  9323  cantnfval2  9559  cottrcl  9609  inlresf1  9808  inrresf1  9810  djuun  9819  dfac12lem2  10036  dfac12a  10040  fin23lem41  10243  dfacfin7  10290  iunfo  10430  gch2  10566  axpre-sup  11060  wrdv  14436  setscom  17091  isofn  17682  homaf  17937  dmaf  17956  cdaf  17957  prdsinvlem  18962  frgpuplem  19685  gsum2dlem2  19884  gsum2d  19885  prdsmgp  20070  rngmgpf  20076  mgpf  20167  prdscrngd  20241  pws1  20244  mulgass3  20272  crngridl  21218  frlmbas  21693  islindf3  21764  psdmul  22082  ply1lss  22110  coe1fval3  22122  coe1tm  22188  ply1coe  22214  evl1expd  22261  pmatcollpw3lem  22699  clsconn  23346  ptbasfi  23497  upxp  23539  uptx  23541  prdstps  23545  hausdiag  23561  cnmpt1st  23584  cnmpt2nd  23585  fbssint  23754  prdstmdd  24040  prdsxmslem2  24445  isngp2  24513  uniiccdif  25507  wlkdlem1  29660  0vfval  30584  xppreima  32625  2ndimaxp  32626  2ndresdju  32629  xppreima2  32631  1stpreimas  32685  fsuppcurry1  32705  fsuppcurry2  32706  ffsrn  32709  gsummpt2d  33027  gsumpart  33035  elrgspnlem2  33208  lindflbs  33342  elrspunidl  33391  dimval  33611  dimvalfi  33612  qtophaus  33847  cnre2csqlem  33921  cntmeas  34237  eulerpartlemmf  34386  eulerpartlemgf  34390  sseqfv1  34400  sseqfn  34401  sseqfv2  34405  coinflippv  34495  fineqvacALT  35138  gblacfnacd  35144  vonf1owev  35150  wevgblacfn  35151  erdszelem2  35234  mpstssv  35581  filnetlem4  36421  bj-0int  37141  bj-idres  37200  elxp8  37411  poimirlem26  37692  poimirlem27  37693  heibor1lem  37855  isnumbasgrplem1  43140  isnumbasgrplem2  43143  dfacbasgrp  43147  resnonrel  43631  comptiunov2i  43745  ntrneiel2  44125  ntrneik4w  44139  conss2  44481  permaxun  45050  permac8prim  45053  slotresfo  48936  basresposfo  49015  ipoglb0  49031  mreclat  49034  isofnALT  49069  rescofuf  49131  initopropdlem  49278  termopropdlem  49279  zeroopropdlem  49280