Theorem ssv 3932

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

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896

This theorem is used by:  inv1  4347  unv  4348  vss  4357  pssv  4361  nvpss  4362  disj2  4410  pwv  4574  unissint  4931  symdifv  5045  trv  5225  intabs  5309  xpss  5666  inxpssres  5667  djussxp  5822  dmv  5903  dmresi  6043  cnvrescnv  6187  imassrn  6197  rescnvcnv  6205  cocnvcnv1  6259  relrelss  6275  fnresi  6668  dffn2  6711  oprabss  7528  fvresex  7972  ofmres  7996  f1stres  8025  f2ndres  8026  fsplitfpar  8131  domssex2  9159  fineqv  9261  fiint  9321  marypha1lem  9428  marypha2  9434  cantnfval2  9673  cottrcl  9723  inlresf1  9999  inrresf1  10001  djuun  10010  dfac12lem2  10226  dfac12a  10230  fin23lem41  10433  dfacfin7  10480  iunfo  10626  gch2  10763  axpre-sup  11257  wrdv  14677  setscom  17363  isofn  17955  homaf  18210  dmaf  18229  cdaf  18230  prdsinvlem  19264  frgpuplem  19991  gsum2dlem2  20190  gsum2d  20191  prdsmgp  20376  rngmgpf  20384  mgpf  20480  prdscrngd  20556  pws1  20559  mulgass3  20588  crngridl  21580  frlmbas  22066  islindf3  22137  psdmul  22492  ply1lss  22519  coe1fval3  22531  coe1tm  22597  ply1coe  22621  evl1expd  22668  pmatcollpw3lem  23106  clsconn  23753  ptbasfi  23905  upxp  23947  uptx  23949  prdstps  23953  hausdiag  23969  cnmpt1st  23992  cnmpt2nd  23993  fbssint  24162  prdstmdd  24448  prdsxmslem2  24853  isngp2  24921  uniiccdif  25904  wlkdlem1  30266  0vfval  31213  xppreima  33286  2ndimaxp  33287  2ndresdju  33290  xppreima2  33292  1stpreimas  33346  fsuppcurry1  33362  fsuppcurry2  33363  ffsrn  33366  gsummpt2d  33656  gsumpart  33670  elrgspnlem2  33850  lindflbs  33980  elrspunidl  34024  dimval  34279  dimvalfi  34280  qtophaus  34514  cnre2csqlem  34588  cntmeas  34905  eulerpartlemmf  35053  eulerpartlemgf  35057  sseqfv1  35067  sseqfn  35068  sseqfv2  35072  coinflippv  35162  werankwe  35791  werankwe2  35792  dfscott2  35796  dfscott3  35797  acwer1prc  35816  fineqvacALT  35841  gblacfnacd  35948  vonf1wev  35955  vonf1owevOLD  35957  wevgblacfn  35958  wevsev  35960  wevonprcf1o  35961  vonf1oonf1  35962  vonf1onprcf1ac  35963  onprcf1of1orad  35972  onprcf1of1orbd  35973  erdszelem2  36043  mpstssv  36390  filnetlem4  37261  regsfromunir1  37420  bj-0int  38114  bj-idres  38174  elxp8  38387  poimirlem26  38657  poimirlem27  38658  heibor1lem  38836  dmsucmap  39493  isnumbasgrplem1  44196  isnumbasgrplem2  44199  dfacbasgrp  44203  resnonrel  44685  comptiunov2i  44799  ntrneiel2  45179  ntrneik4w  45193  conss2  45519  permaxun  46094  permac8prim  46097  ishfstruct  46121  sqrtnpoly  48036  slotresfo  50106  basresposfo  50185  ipoglb0  50201  mreclat  50204  isofnALT  50238  rescofuf  50301  initopropdlem  50455  termopropdlem  50456  zeroopropdlem  50457