Theorem ssv 3625

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

Syntax hints:  Vcvv 3200   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  inv1  3970  unv  3971  vss  4012  pssv  4016  disj2  4024  pwv  4433  unissint  4501  symdifv  4598  trv  4765  intabs  4825  xpss  5226  djussxp  5267  dmv  5341  dmresi  5457  resid  5460  ssrnres  5572  rescnvcnv  5597  cocnvcnv1  5646  relrelss  5659  dffn2  6047  oprabss  6746  fvresex  7139  ofmres  7164  f1stres  7190  f2ndres  7191  domssex2  8120  fineqv  8175  fiint  8237  marypha1lem  8339  marypha2  8345  cantnfval2  8566  oef1o  8595  dfac12lem2  8966  dfac12a  8970  fin23lem41  9174  dfacfin7  9221  iunfo  9361  gch2  9497  axpre-sup  9990  wrdv  13320  setscom  15903  isofn  16435  homaf  16680  dmaf  16699  cdaf  16700  prdsinvlem  17524  frgpuplem  18185  gsum2dlem2  18370  gsum2d  18371  mgpf  18559  prdsmgp  18610  prdscrngd  18613  pws1  18616  mulgass3  18637  crngridl  19238  ply1lss  19566  coe1fval3  19578  coe1tm  19643  ply1coe  19666  evl1expd  19709  frlmbas  20099  islindf3  20165  pmatcollpw3lem  20588  clsconn  21233  ptbasfi  21384  upxp  21426  uptx  21428  prdstps  21432  hausdiag  21448  cnmptid  21464  cnmpt1st  21471  cnmpt2nd  21472  fbssint  21642  prdstmdd  21927  prdsxmslem2  22334  isngp2  22401  uniiccdif  23346  wlkdlem1  26579  0vfval  27461  xppreima  29449  xppreima2  29450  1stpreimas  29483  ffsrn  29504  gsummpt2d  29781  qtophaus  29903  cnre2csqlem  29956  cntmeas  30289  eulerpartlemmf  30437  eulerpartlemgf  30441  sseqfv1  30451  sseqfn  30452  sseqfv2  30456  coinflippv  30545  erdszelem2  31174  mpstssv  31436  filnetlem4  32376  bj-0int  33055  elxp8  33219  poimirlem16  33425  poimirlem19  33428  poimirlem20  33429  poimirlem26  33435  poimirlem27  33436  heibor1lem  33608  inxpssres  34076  rmxyelqirr  37475  isnumbasgrplem1  37671  isnumbasgrplem2  37674  dfacbasgrp  37678  resnonrel  37898  comptiunov2i  37998  ntrneiel2  38384  ntrneik4w  38398  compneOLD  38644  conss2  38647