Theorem ssv 4020

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

Syntax hints:  Vcvv 3478   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980

This theorem is referenced by:  inv1  4404  unv  4405  vss  4452  pssv  4455  disj2  4464  pwv  4909  unissint  4977  symdifv  5091  trv  5279  intabs  5355  xpss  5705  inxpssres  5706  djussxp  5859  dmv  5936  dmresi  6072  cnvrescnv  6217  rescnvcnv  6226  cocnvcnv1  6279  relrelss  6295  fnresi  6698  dffn2  6739  oprabss  7540  fvresex  7983  ofmres  8008  f1stres  8037  f2ndres  8038  fsplitfpar  8142  domssex2  9176  fineqv  9297  fiint  9364  fiintOLD  9365  marypha1lem  9471  marypha2  9477  cantnfval2  9707  cottrcl  9757  inlresf1  9953  inrresf1  9955  djuun  9964  dfac12lem2  10183  dfac12a  10187  fin23lem41  10390  dfacfin7  10437  iunfo  10577  gch2  10713  axpre-sup  11207  wrdv  14564  setscom  17214  isofn  17823  homaf  18084  dmaf  18103  cdaf  18104  prdsinvlem  19080  frgpuplem  19805  gsum2dlem2  20004  gsum2d  20005  prdsmgp  20169  rngmgpf  20175  mgpf  20266  prdscrngd  20336  pws1  20339  mulgass3  20370  crngridl  21308  frlmbas  21793  islindf3  21864  psdmul  22188  ply1lss  22214  coe1fval3  22226  coe1tm  22292  ply1coe  22318  evl1expd  22365  pmatcollpw3lem  22805  clsconn  23454  ptbasfi  23605  upxp  23647  uptx  23649  prdstps  23653  hausdiag  23669  cnmpt1st  23692  cnmpt2nd  23693  fbssint  23862  prdstmdd  24148  prdsxmslem2  24558  isngp2  24626  uniiccdif  25627  wlkdlem1  29715  0vfval  30635  xppreima  32662  2ndimaxp  32663  2ndresdju  32666  xppreima2  32668  1stpreimas  32721  fsuppcurry1  32743  fsuppcurry2  32744  ffsrn  32747  gsummpt2d  33035  gsumpart  33043  elrgspnlem2  33233  lindflbs  33387  elrspunidl  33436  dimval  33628  dimvalfi  33629  qtophaus  33797  cnre2csqlem  33871  cntmeas  34207  eulerpartlemmf  34357  eulerpartlemgf  34361  sseqfv1  34371  sseqfn  34372  sseqfv2  34376  coinflippv  34465  fineqvacALT  35091  gblacfnacd  35092  wevgblacfn  35093  erdszelem2  35177  mpstssv  35524  filnetlem4  36364  bj-0int  37084  bj-idres  37143  elxp8  37354  poimirlem26  37633  poimirlem27  37634  heibor1lem  37796  rmxyelqirrOLD  42899  isnumbasgrplem1  43090  isnumbasgrplem2  43093  dfacbasgrp  43097  resnonrel  43582  comptiunov2i  43696  ntrneiel2  44076  ntrneik4w  44090  conss2  44439  ipoglb0  48783  mreclat  48786