Theorem ssv 3971

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

Syntax hints:  Vcvv 3446   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  inv1  4359  unv  4360  vss  4408  pssv  4411  disj2  4422  pwv  4867  unissint  4938  symdifv  5051  trv  5241  intabs  5304  xpss  5654  inxpssres  5655  djussxp  5806  dmv  5883  dmresi  6010  cnvrescnv  6152  rescnvcnv  6161  cocnvcnv1  6214  relrelss  6230  fnresi  6635  dffn2  6675  oprabss  7468  fvresex  7897  ofmres  7922  f1stres  7950  f2ndres  7951  fsplitfpar  8055  domssex2  9088  fineqv  9214  fiint  9275  marypha1lem  9378  marypha2  9384  cantnfval2  9614  cottrcl  9664  inlresf1  9860  inrresf1  9862  djuun  9871  dfac12lem2  10089  dfac12a  10093  fin23lem41  10297  dfacfin7  10344  iunfo  10484  gch2  10620  axpre-sup  11114  wrdv  14429  setscom  17063  isofn  17672  homaf  17930  dmaf  17949  cdaf  17950  prdsinvlem  18870  frgpuplem  19568  gsum2dlem2  19762  gsum2d  19763  mgpf  19993  prdsmgp  20048  prdscrngd  20051  pws1  20054  mulgass3  20080  crngridl  20767  frlmbas  21198  islindf3  21269  ply1lss  21604  coe1fval3  21616  coe1tm  21681  ply1coe  21704  evl1expd  21748  pmatcollpw3lem  22169  clsconn  22818  ptbasfi  22969  upxp  23011  uptx  23013  prdstps  23017  hausdiag  23033  cnmpt1st  23056  cnmpt2nd  23057  fbssint  23226  prdstmdd  23512  prdsxmslem2  23922  isngp2  23990  uniiccdif  24979  wlkdlem1  28693  0vfval  29611  xppreima  31629  2ndimaxp  31630  2ndresdju  31632  xppreima2  31634  1stpreimas  31687  fsuppcurry1  31710  fsuppcurry2  31711  ffsrn  31714  gsummpt2d  31961  gsumpart  31967  lindflbs  32239  elrspunidl  32279  dimval  32384  dimvalfi  32385  qtophaus  32506  cnre2csqlem  32580  cntmeas  32914  eulerpartlemmf  33064  eulerpartlemgf  33068  sseqfv1  33078  sseqfn  33079  sseqfv2  33083  coinflippv  33172  fineqvacALT  33788  erdszelem2  33873  mpstssv  34220  filnetlem4  34929  bj-0int  35645  bj-idres  35704  elxp8  35915  poimirlem26  36177  poimirlem27  36178  heibor1lem  36341  rmxyelqirrOLD  41292  isnumbasgrplem1  41486  isnumbasgrplem2  41489  dfacbasgrp  41493  resnonrel  41986  comptiunov2i  42100  ntrneiel2  42480  ntrneik4w  42494  conss2  42845  ipoglb0  47139  mreclat  47142