Theorem ssv 4006

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

Syntax hints:  Vcvv 3473   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  inv1  4398  unv  4399  vss  4447  pssv  4450  disj2  4461  pwv  4909  unissint  4979  symdifv  5093  trv  5283  intabs  5348  xpss  5698  inxpssres  5699  djussxp  5852  dmv  5929  dmresi  6060  cnvrescnv  6204  rescnvcnv  6213  cocnvcnv1  6266  relrelss  6282  fnresi  6689  dffn2  6729  oprabss  7533  fvresex  7969  ofmres  7994  f1stres  8023  f2ndres  8024  fsplitfpar  8129  domssex2  9168  fineqv  9294  fiint  9356  marypha1lem  9464  marypha2  9470  cantnfval2  9700  cottrcl  9750  inlresf1  9946  inrresf1  9948  djuun  9957  dfac12lem2  10175  dfac12a  10179  fin23lem41  10383  dfacfin7  10430  iunfo  10570  gch2  10706  axpre-sup  11200  wrdv  14519  setscom  17156  isofn  17765  homaf  18026  dmaf  18045  cdaf  18046  prdsinvlem  19012  frgpuplem  19734  gsum2dlem2  19933  gsum2d  19934  prdsmgp  20098  rngmgpf  20104  mgpf  20195  prdscrngd  20265  pws1  20268  mulgass3  20299  crngridl  21179  frlmbas  21696  islindf3  21767  psdmul  22097  ply1lss  22122  coe1fval3  22134  coe1tm  22199  ply1coe  22224  evl1expd  22271  pmatcollpw3lem  22705  clsconn  23354  ptbasfi  23505  upxp  23547  uptx  23549  prdstps  23553  hausdiag  23569  cnmpt1st  23592  cnmpt2nd  23593  fbssint  23762  prdstmdd  24048  prdsxmslem2  24458  isngp2  24526  uniiccdif  25527  wlkdlem1  29516  0vfval  30436  xppreima  32453  2ndimaxp  32454  2ndresdju  32456  xppreima2  32458  1stpreimas  32506  fsuppcurry1  32528  fsuppcurry2  32529  ffsrn  32532  gsummpt2d  32784  gsumpart  32790  lindflbs  33119  elrspunidl  33169  dimval  33331  dimvalfi  33332  qtophaus  33470  cnre2csqlem  33544  cntmeas  33878  eulerpartlemmf  34028  eulerpartlemgf  34032  sseqfv1  34042  sseqfn  34043  sseqfv2  34047  coinflippv  34136  fineqvacALT  34751  erdszelem2  34835  mpstssv  35182  filnetlem4  35898  bj-0int  36613  bj-idres  36672  elxp8  36883  poimirlem26  37152  poimirlem27  37153  heibor1lem  37315  rmxyelqirrOLD  42362  isnumbasgrplem1  42556  isnumbasgrplem2  42559  dfacbasgrp  42563  resnonrel  43053  comptiunov2i  43167  ntrneiel2  43547  ntrneik4w  43561  conss2  43911  ipoglb0  48083  mreclat  48086