Theorem ssv 4007

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

Syntax hints:  Vcvv 3475   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  inv1  4395  unv  4396  vss  4444  pssv  4447  disj2  4458  pwv  4906  unissint  4977  symdifv  5090  trv  5280  intabs  5343  xpss  5693  inxpssres  5694  djussxp  5846  dmv  5923  dmresi  6052  cnvrescnv  6195  rescnvcnv  6204  cocnvcnv1  6257  relrelss  6273  fnresi  6680  dffn2  6720  oprabss  7515  fvresex  7946  ofmres  7971  f1stres  7999  f2ndres  8000  fsplitfpar  8104  domssex2  9137  fineqv  9263  fiint  9324  marypha1lem  9428  marypha2  9434  cantnfval2  9664  cottrcl  9714  inlresf1  9910  inrresf1  9912  djuun  9921  dfac12lem2  10139  dfac12a  10143  fin23lem41  10347  dfacfin7  10394  iunfo  10534  gch2  10670  axpre-sup  11164  wrdv  14479  setscom  17113  isofn  17722  homaf  17980  dmaf  17999  cdaf  18000  prdsinvlem  18932  frgpuplem  19640  gsum2dlem2  19839  gsum2d  19840  mgpf  20071  prdsmgp  20132  prdscrngd  20135  pws1  20138  mulgass3  20167  crngridl  20876  frlmbas  21310  islindf3  21381  ply1lss  21720  coe1fval3  21732  coe1tm  21795  ply1coe  21820  evl1expd  21864  pmatcollpw3lem  22285  clsconn  22934  ptbasfi  23085  upxp  23127  uptx  23129  prdstps  23133  hausdiag  23149  cnmpt1st  23172  cnmpt2nd  23173  fbssint  23342  prdstmdd  23628  prdsxmslem2  24038  isngp2  24106  uniiccdif  25095  wlkdlem1  28939  0vfval  29859  xppreima  31871  2ndimaxp  31872  2ndresdju  31874  xppreima2  31876  1stpreimas  31927  fsuppcurry1  31950  fsuppcurry2  31951  ffsrn  31954  gsummpt2d  32201  gsumpart  32207  lindflbs  32495  elrspunidl  32546  dimval  32686  dimvalfi  32687  qtophaus  32816  cnre2csqlem  32890  cntmeas  33224  eulerpartlemmf  33374  eulerpartlemgf  33378  sseqfv1  33388  sseqfn  33389  sseqfv2  33393  coinflippv  33482  fineqvacALT  34098  erdszelem2  34183  mpstssv  34530  filnetlem4  35266  bj-0int  35982  bj-idres  36041  elxp8  36252  poimirlem26  36514  poimirlem27  36515  heibor1lem  36677  rmxyelqirrOLD  41649  isnumbasgrplem1  41843  isnumbasgrplem2  41846  dfacbasgrp  41850  resnonrel  42343  comptiunov2i  42457  ntrneiel2  42837  ntrneik4w  42851  conss2  43202  rngmgpf  46653  ipoglb0  47619  mreclat  47622