Theorem ssv 3962

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

Syntax hints:  Vcvv 3455   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923

This theorem is referenced by:  inv1  4356  unv  4357  vss  4366  pssv  4370  nvpss  4371  disj2  4419  pwv  4870  unissint  4938  symdifv  5053  trv  5233  intabs  5321  xpss  5679  inxpssres  5680  djussxp  5833  dmv  5914  dmresi  6056  cnvrescnv  6196  rescnvcnv  6207  cocnvcnv1  6261  relrelss  6276  fnresi  6666  dffn2  6709  oprabss  7520  fvresex  7958  ofmres  7982  f1stres  8011  f2ndres  8012  fsplitfpar  8114  domssex2  9126  fineqv  9228  fiint  9287  marypha1lem  9394  marypha2  9400  cantnfval2  9639  cottrcl  9689  inlresf1  9902  inrresf1  9904  djuun  9913  dfac12lem2  10129  dfac12a  10133  fin23lem41  10337  dfacfin7  10384  iunfo  10524  gch2  10661  axpre-sup  11155  wrdv  14568  setscom  17241  isofn  17833  homaf  18088  dmaf  18107  cdaf  18108  prdsinvlem  19116  frgpuplem  19843  gsum2dlem2  20042  gsum2d  20043  prdsmgp  20228  rngmgpf  20236  mgpf  20331  prdscrngd  20404  pws1  20407  mulgass3  20436  crngridl  21400  frlmbas  21886  islindf3  21957  psdmul  22310  ply1lss  22337  coe1fval3  22349  coe1tm  22415  ply1coe  22439  evl1expd  22486  pmatcollpw3lem  22921  clsconn  23568  ptbasfi  23719  upxp  23761  uptx  23763  prdstps  23767  hausdiag  23783  cnmpt1st  23806  cnmpt2nd  23807  fbssint  23976  prdstmdd  24262  prdsxmslem2  24667  isngp2  24735  uniiccdif  25718  wlkdlem1  30011  0vfval  30939  xppreima  32971  2ndimaxp  32972  2ndresdju  32975  xppreima2  32977  1stpreimas  33032  fsuppcurry1  33050  fsuppcurry2  33051  ffsrn  33054  gsummpt2d  33350  gsumpart  33364  elrgspnlem2  33544  lindflbs  33673  elrspunidl  33717  dimval  33972  dimvalfi  33973  qtophaus  34207  cnre2csqlem  34281  cntmeas  34597  eulerpartlemmf  34746  eulerpartlemgf  34750  sseqfv1  34760  sseqfn  34761  sseqfv2  34765  coinflippv  34855  dfscott2  35492  dfscott3  35493  fineqvacALT  35511  gblacfnacd  35567  vonf1wev  35573  vonf1owevOLD  35575  wevgblacfn  35576  wevonprcf1o  35578  vonf1oonf1  35579  erdszelem2  35665  mpstssv  36012  filnetlem4  36873  regsfromunir1  37032  bj-0int  37724  bj-idres  37785  elxp8  37998  poimirlem26  38278  poimirlem27  38279  heibor1lem  38441  dmsucmap  39098  isnumbasgrplem1  43811  isnumbasgrplem2  43814  dfacbasgrp  43818  resnonrel  44301  comptiunov2i  44415  ntrneiel2  44795  ntrneik4w  44809  conss2  45135  permaxun  45703  permac8prim  45706  slotresfo  49660  basresposfo  49739  ipoglb0  49755  mreclat  49758  isofnALT  49792  rescofuf  49854  initopropdlem  50001  termopropdlem  50002  zeroopropdlem  50003