Theorem ssv 3587

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

Syntax hints:  Vcvv 3172   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174  df-in 3546  df-ss 3553

This theorem is referenced by:  inv1  3921  unv  3922  vss  3963  pssv  3967  disj2  3975  pwv  4365  unissint  4430  symdifv  4528  trv  4687  intabs  4747  xpss  5138  djussxp  5177  dmv  5249  dmresi  5363  resid  5366  ssrnres  5477  rescnvcnv  5501  cocnvcnv1  5549  relrelss  5562  dffn2  5946  oprabss  6622  fvresex  7009  ofmres  7032  f1stres  7058  f2ndres  7059  domssex2  7982  fineqv  8037  fiint  8099  marypha1lem  8199  marypha2  8205  cantnfval2  8426  oef1o  8455  dfac12lem2  8826  dfac12a  8830  fin23lem41  9034  dfacfin7  9081  iunfo  9217  gch2  9353  axpre-sup  9846  wrdv  13121  setscom  15677  isofn  16204  homaf  16449  dmaf  16468  cdaf  16469  prdsinvlem  17293  frgpuplem  17954  gsum2dlem2  18139  gsum2d  18140  mgpf  18328  prdsmgp  18379  prdscrngd  18382  pws1  18385  mulgass3  18406  crngridl  19005  ply1lss  19333  coe1fval3  19345  coe1tm  19410  ply1coe  19433  evl1expd  19476  frlmbas  19860  islindf3  19926  pmatcollpw3lem  20349  clscon  20985  ptbasfi  21136  upxp  21178  uptx  21180  prdstps  21184  hausdiag  21200  cnmptid  21216  cnmpt1st  21223  cnmpt2nd  21224  fbssint  21394  prdstmdd  21679  prdsxmslem2  22085  isngp2  22152  uniiccdif  23069  0vfval  26629  xppreima  28635  xppreima2  28636  1stpreimas  28672  ffsrn  28698  gsummpt2d  28918  qtophaus  29037  cnre2csqlem  29090  cntmeas  29422  eulerpartlemmf  29570  eulerpartlemgf  29574  sseqfv1  29584  sseqfn  29585  sseqfv2  29589  coinflippv  29678  erdszelem2  30234  mpstssv  30496  filnetlem4  31352  elxp8  32198  poimirlem16  32398  poimirlem19  32401  poimirlem20  32402  poimirlem26  32408  poimirlem27  32409  heibor1lem  32581  rmxyelqirr  36296  isnumbasgrplem1  36493  isnumbasgrplem2  36496  dfacbasgrp  36500  resnonrel  36720  comptiunov2i  36820  ntrneiel2  37207  ntrneik4w  37221  compne  37468  conss2  37471  1wlkdlem1  40893