Theorem ssv 3658

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

Syntax hints:  Vcvv 3231   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-in 3614  df-ss 3621

This theorem is referenced by:  inv1  4003  unv  4004  vss  4045  pssv  4049  disj2  4057  pwv  4465  unissint  4533  symdifv  4630  trv  4798  intabs  4855  xpss  5159  djussxp  5300  dmv  5373  dmresi  5492  residOLD  5495  ssrnres  5607  rescnvcnv  5632  cocnvcnv1  5684  relrelss  5697  dffn2  6085  oprabss  6788  fvresex  7181  ofmres  7206  f1stres  7234  f2ndres  7235  domssex2  8161  fineqv  8216  fiint  8278  marypha1lem  8380  marypha2  8386  cantnfval2  8604  oef1o  8633  dfac12lem2  9004  dfac12a  9008  fin23lem41  9212  dfacfin7  9259  iunfo  9399  gch2  9535  axpre-sup  10028  wrdv  13352  setscom  15950  isofn  16482  homaf  16727  dmaf  16746  cdaf  16747  prdsinvlem  17571  frgpuplem  18231  gsum2dlem2  18416  gsum2d  18417  mgpf  18605  prdsmgp  18656  prdscrngd  18659  pws1  18662  mulgass3  18683  crngridl  19286  ply1lss  19614  coe1fval3  19626  coe1tm  19691  ply1coe  19714  evl1expd  19757  frlmbas  20147  islindf3  20213  pmatcollpw3lem  20636  clsconn  21281  ptbasfi  21432  upxp  21474  uptx  21476  prdstps  21480  hausdiag  21496  cnmptid  21512  cnmpt1st  21519  cnmpt2nd  21520  fbssint  21689  prdstmdd  21974  prdsxmslem2  22381  isngp2  22448  uniiccdif  23392  wlkdlem1  26635  0vfval  27589  xppreima  29577  xppreima2  29578  1stpreimas  29611  ffsrn  29632  gsummpt2d  29909  qtophaus  30031  cnre2csqlem  30084  cntmeas  30417  eulerpartlemmf  30565  eulerpartlemgf  30569  sseqfv1  30579  sseqfn  30580  sseqfv2  30584  coinflippv  30673  erdszelem2  31300  mpstssv  31562  filnetlem4  32501  bj-0int  33180  elxp8  33349  poimirlem16  33555  poimirlem19  33558  poimirlem20  33559  poimirlem26  33565  poimirlem27  33566  heibor1lem  33738  inxpssres  34217  rmxyelqirr  37792  isnumbasgrplem1  37988  isnumbasgrplem2  37991  dfacbasgrp  37995  resnonrel  38215  comptiunov2i  38315  ntrneiel2  38701  ntrneik4w  38715  compneOLD  38961  conss2  38964