Theorem ssv 3821

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

Syntax hints:  Vcvv 3385   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-v 3387  df-in 3776  df-ss 3783

This theorem is referenced by:  inv1  4166  unv  4167  vss  4208  pssv  4211  disj2  4220  pwv  4625  unissint  4691  symdifv  4788  trv  4957  intabs  5017  xpss  5328  inxpssres  5329  djussxp  5471  dmv  5544  residOLD  5649  dmresi  5676  rescnvcnv  5813  cocnvcnv1  5865  relrelss  5878  dffn2  6258  oprabss  6980  fvresex  7374  ofmres  7397  f1stres  7425  f2ndres  7426  domssex2  8362  fineqv  8417  fiint  8479  marypha1lem  8581  marypha2  8587  cantnfval2  8816  oef1o  8845  inlresf1  9027  inrresf1  9029  djuun  9038  dfac12lem2  9254  dfac12a  9258  fin23lem41  9462  dfacfin7  9509  iunfo  9649  gch2  9785  axpre-sup  10278  wrdv  13549  setscom  16228  isofn  16749  homaf  16994  dmaf  17013  cdaf  17014  prdsinvlem  17840  frgpuplem  18500  gsum2dlem2  18685  gsum2d  18686  mgpf  18875  prdsmgp  18926  prdscrngd  18929  pws1  18932  mulgass3  18953  crngridl  19561  ply1lss  19888  coe1fval3  19900  coe1tm  19965  ply1coe  19988  evl1expd  20031  frlmbas  20424  islindf3  20490  pmatcollpw3lem  20916  clsconn  21562  ptbasfi  21713  upxp  21755  uptx  21757  prdstps  21761  hausdiag  21777  cnmptid  21793  cnmpt1st  21800  cnmpt2nd  21801  fbssint  21970  prdstmdd  22255  prdsxmslem2  22662  isngp2  22729  uniiccdif  23686  wlkdlem1  26935  0vfval  27986  xppreima  29968  xppreima2  29969  1stpreimas  30001  ffsrn  30022  gsummpt2d  30297  qtophaus  30419  cnre2csqlem  30472  cntmeas  30805  eulerpartlemmf  30953  eulerpartlemgf  30957  sseqfv1  30968  sseqfn  30969  sseqfv2  30973  coinflippv  31062  erdszelem2  31691  mpstssv  31953  filnetlem4  32888  bj-0int  33548  elxp8  33717  poimirlem16  33914  poimirlem19  33917  poimirlem20  33918  poimirlem26  33924  poimirlem27  33925  heibor1lem  34095  rmxyelqirr  38260  isnumbasgrplem1  38456  isnumbasgrplem2  38459  dfacbasgrp  38463  resnonrel  38681  comptiunov2i  38781  ntrneiel2  39166  ntrneik4w  39180  compneOLD  39425  conss2  39427