Theorem ssv 3937

Description: Any class is a subclass of the universal class. Dual of 0ss 4353. (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 3475	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3917	1 ⊢ 𝐴 ⊆ V

This proof depends on syntax axioms:  Vcvv 3454   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901

This theorem is used by:  inv1  4351  unv  4352  vss  4361  pssv  4365  nvpss  4366  disj2  4414  pwv  4578  unissint  4935  symdifv  5049  trv  5229  intabs  5314  xpss  5671  inxpssres  5672  djussxp  5829  dmv  5911  dmresi  6056  cnvrescnv  6200  imassrn  6210  rescnvcnv  6218  cocnvcnv1  6272  relrelss  6293  fnresi  6690  dffn2  6733  oprabss  7551  fvresex  7996  ofmres  8020  f1stres  8049  f2ndres  8050  fsplitfpar  8156  domssex2  9184  fineqv  9286  fiint  9346  marypha1lem  9452  marypha2  9458  cantnfval2  9697  cottrcl  9747  inlresf1  10023  inrresf1  10025  djuun  10034  dfac12lem2  10250  dfac12a  10254  fin23lem41  10457  dfacfin7  10504  iunfo  10650  gch2  10787  axpre-sup  11281  wrdv  14701  setscom  17387  isofn  17979  homaf  18234  dmaf  18253  cdaf  18254  prdsinvlem  19288  frgpuplem  20016  gsum2dlem2  20215  gsum2d  20216  prdsmgp  20401  rngmgpf  20409  mgpf  20505  prdscrngd  20581  pws1  20584  mulgass3  20613  crngridl  21605  frlmbas  22091  islindf3  22162  psdmul  22517  ply1lss  22544  coe1fval3  22556  coe1tm  22622  ply1coe  22646  evl1expd  22693  pmatcollpw3lem  23131  clsconn  23778  ptbasfi  23930  upxp  23972  uptx  23974  prdstps  23978  hausdiag  23994  cnmpt1st  24017  cnmpt2nd  24018  fbssint  24187  prdstmdd  24473  prdsxmslem2  24878  isngp2  24946  uniiccdif  25929  wlkdlem1  30291  0vfval  31238  xppreima  33311  2ndimaxp  33312  2ndresdju  33315  xppreima2  33317  1stpreimas  33370  fsuppcurry1  33386  fsuppcurry2  33387  ffsrn  33390  gsummpt2d  33680  gsumpart  33694  elrgspnlem2  33874  lindflbs  34004  elrspunidl  34048  dimval  34303  dimvalfi  34304  qtophaus  34538  cnre2csqlem  34612  cntmeas  34929  eulerpartlemmf  35077  eulerpartlemgf  35081  sseqfv1  35091  sseqfn  35092  sseqfv2  35096  coinflippv  35186  werankwe  35821  werankwe2  35822  dfscott2  35826  dfscott3  35827  acwer1prc  35852  fineqvacALT  35885  gblacfnacd  36029  vonf1wev  36036  vonf1owevOLD  36038  wevgblacfn  36039  wevsev  36041  wevonprcf1o  36042  vonf1oonf1  36043  vonf1onprcf1ac  36044  onprcf1of1orad  36053  onprcf1of1orbd  36054  erdszelem2  36124  mpstssv  36471  filnetlem4  37347  regsfromunir1  37506  bj-0int  38213  bj-idres  38273  elxp8  38486  poimirlem26  38756  poimirlem27  38757  heibor1lem  38935  dmsucmap  39592  isnumbasgrplem1  44295  isnumbasgrplem2  44298  dfacbasgrp  44302  resnonrel  44784  comptiunov2i  44898  ntrneiel2  45278  ntrneik4w  45292  conss2  45617  permaxun  46196  permac8prim  46199  ishfstruct  46226  sqrtnpoly  48148  slotresfo  50218  basresposfo  50297  ipoglb0  50313  mreclat  50316  isofnALT  50350  rescofuf  50413  initopropdlem  50567  termopropdlem  50568  zeroopropdlem  50569